A Theory of Generalised Substitutions
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.
KeywordsGeneralise Substitution Parallel Composition Abstract Machine Characteristic List Active Frame
Unable to display preview. Download preview PDF.
- 1.J.-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.Google Scholar
- 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.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.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.E.W. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976.Google Scholar
- 11.C.A.R. Hoare and He Jifeng. Unifying Theories of Programming. Prentice Hall, 1998.Google Scholar
- 12.C.B. Jones. Systematic Software Development Using VDM (2nd edn). Prentice-Hall, 1990.Google Scholar
- 13.C.C. Morgan. The specification statement. ACM Transactions on Programming Languages and Systems, 10(3), 1988.Google Scholar
- 14.C.C. Morgan. Programming from Specifications (2nd edn). Prentice Hall International, 1994.Google Scholar
- 16.G. Nelson. A generalisation of Dijkstra’s calculus. ACM Transactions on Programmg Languages and Systems, 11(4), 1989.Google Scholar
- 20.J. Woodcock and J. Davies. Using Z: Specification, Refinement and Proof. Prentice Hall, 1996.Google Scholar