A Theory of Generalised Substitutions

  • Steve Dunne
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2272)


We augment the usual wp semantics of substitutions with an explicit notion of frame, which allows us to develop a simple selfcontained theory of generalised substitutions outside their usual context of the B Method. We formulate three fundamental healthiness conditions which semantically characterise all substitutions, and from which we are able to derive directly, without need of any explicit further appeal to syntax, a number of familiar properties of substitutions, as well as several new ones specifically concerning frames. In doing so we gain some useful insights about the nature of substitutions, which enables us to resolve some hitherto problematic issues concerning substitutions within the B Method.


Generalise Substitution Parallel Composition Abstract Machine Characteristic List Active Frame 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J.-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.Google Scholar
  2. 2.
    R.-J. Back. A calculus of refinements for program derivations. Acta Informatica, 25:593–624, 1988.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    R.-J. Back and M.J. Butler. Fusion and simultaneous execution in the refinement calculus. Acta Informatica, 35(11):921–940, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    R.-J. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Springer-Verlag New York, 1998.zbMATHGoogle Scholar
  5. 5.
    D. Bert, M.-L. Potet, and Y. Rouzaud. A study on components and assembly primitives in B. In H. Habrias, editor, Proceedings of the First B Conference, pages 47–62. IRIN, Nantes, 1996.Google Scholar
  6. 6.
    J.C. Bicarregui and B. Ritchie. Invariants, frames and postconditions: a comparison of the VDM and B notations. In J. Woodcock and P.G. Larsen, editors, Proceedings of FME’93, number 670 in Lecture Notes in Computer Science. Springer-Verlag, 1993.Google Scholar
  7. 7.
    P Chartier. Formalisation of B in Isabelle/HOL. In D. Bert, editor, B’98: Recent Advances in the Development and Use of the B Method; Proceedings of the Second International B Conference, Montpellier, France, number 1393 in Lecture Notes in Computer Science, pages 66–82. Springer-Verlag, 1998.CrossRefGoogle Scholar
  8. 8.
    E.W. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976.Google Scholar
  9. 9.
    S.E. Dunne. The Safe Machine: a new specification construct for B. In J.M. Wing, J. Woodcock, and J. Davies, editors, FM’99-Formal Methods, number 1708 in Lecture Notes in Computer Science, pages 472–489. Springer-Verlag, 1999.CrossRefGoogle Scholar
  10. 10.
    R.W. Floyd. Assigning meanings to programs. Proceedings of Symposia in Applied Mathematics, 19:19–32, 1967.MathSciNetGoogle Scholar
  11. 11.
    C.A.R. Hoare and He Jifeng. Unifying Theories of Programming. Prentice Hall, 1998.Google Scholar
  12. 12.
    C.B. Jones. Systematic Software Development Using VDM (2nd edn). Prentice-Hall, 1990.Google Scholar
  13. 13.
    C.C. Morgan. The specification statement. ACM Transactions on Programming Languages and Systems, 10(3), 1988.Google Scholar
  14. 14.
    C.C. Morgan. Programming from Specifications (2nd edn). Prentice Hall International, 1994.Google Scholar
  15. 15.
    J.M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer programming, 9:287–306, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    G. Nelson. A generalisation of Dijkstra’s calculus. ACM Transactions on Programmg Languages and Systems, 11(4), 1989.Google Scholar
  17. 17.
    Y. Rouzaud. Interpreting the B-Method in the Refinement Calculus. In J.M. Wing, J. Woodcock, and J. Davies, editors, FM’99-Formal Methods, number 1708 in Lecture Notes in Computer Science, pages 411–430. Springer-Verlag, 1999.CrossRefGoogle Scholar
  18. 18.
    G. Smith. Recursive schema definitions in Object-Z. In J.P. Bowen, S.E. Dunne, A. Galloway, and S. King, editors, ZB2000: Formal Specification and Development in B and Z, number 1878 in Lecture Notes in Computer Science, pages 42–58. Springer-Verlag, 2000.CrossRefGoogle Scholar
  19. 19.
    A. Tarski. A lattice theoretical fixed point theorem and its applications. Pacific Journal of Mathematics, 5:285–309, 1955.zbMATHMathSciNetGoogle Scholar
  20. 20.
    J. Woodcock and J. Davies. Using Z: Specification, Refinement and Proof. Prentice Hall, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Steve Dunne
    • 1
  1. 1.School of Computing and MathematicsUniversity of TeessideMiddlesbroughUK

Personalised recommendations