Advertisement

A Prospective-Value Semantics for the GSL

  • Frank Zeyda
  • Bill Stoddart
  • Steve Dunne
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3455)

Abstract

We present a prospective-value (pv) semantics for the Generalised Substitution Language. Whereas wp semantics captures the meaning of a computation in terms of the weakest precondition that must be fulfilled for a generalised substitution S to establish any given postcondition Q, pv semantics expresses the meaning of a computation in terms of the value any expression E would take were the computation to be carried out. To integrate non-termination we formulate improper bunch theory, an extended version of Hehner’s bunch theory where each type is augmented with an improper bunch. Algebraic simplification laws for the pv expression transformer are presented, and proved to be sound. Iteration is treated as a fixed-point in expressions, and a corresponding theorem is presented allowing us to infer the pv effect of the while-loop construct.

Keywords

Generalised substitution bunch theory prospective-value semantics expression transformers wp calculus B Method 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)zbMATHCrossRefGoogle Scholar
  2. 2.
    Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, Heidelberg (1998)zbMATHGoogle Scholar
  3. 3.
    Dunne, S.: A theory of generalised substitutions. In: Bert, D., P. Bowen, J., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 270–290. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  4. 4.
    Hehner, E.C.R.: Bunch theory: A simple set theory for computer science. Information Processing Letters 12(1), 26–30 (1981)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Hehner, E.C.R.: A Practical Theory of Programming. Texts and Monographs in Computer Science. Springer, Heidelberg (1993)zbMATHGoogle Scholar
  6. 6.
    Morris, J.M., Bunkenburg, A.: A theory of bunches. Acta Informatica 37(8), 541–561 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Stoddart, W.J., Zeyda, F.: Expression transformers in B-GSL. In: Bert, D., P. Bowen, J., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 197–215. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  8. 8.
    Tarski, A.: A lattice-theoretical fixed-point theorem and its applications. Pacific Journal of Mathematics 5, 285–309 (1955)zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Frank Zeyda
    • 1
  • Bill Stoddart
    • 1
  • Steve Dunne
    • 1
  1. 1.School of ComputingUniversity of TeessideMiddlesbroughUK

Personalised recommendations