Algorithm refinement with read and write frames

  • Juan Bicarregui
Part of the Lecture Notes in Computer Science book series (LNCS, volume 670)


The read and write frames of reference variables used in the VDM style of operation decomposition serve two purposes. Syntactically, they bind the variables that occur in the predicates of the operation specification; and semantically, they record what access to the state an implementation can be allowed to make. This paper examines the use of frames in these two roles, in particular considering the case when there is an invariant on the state. It argues that the two roles can be usefully distinguished.

A model for operation specification and refinement is developed where full account is taken of both syntactic and semantic roles of the frames. Consideration of their syntactic role gives rise to the idea that a part of the state can be independent of the rest with respect to the invariant that is in force: a definition of independence is given together with a syntactic sufficient-condition for it. The semantic role of the frames is examined in connection with notions of satisfiability and satisfaction. Satisfiability is modified to capture the restricted possible interdependencies between read and write variables and the rules for satisfaction are given that restrict the usual relation in order to respect the constraints on implementations imposed by the frames.


Free Variable Operation Specification Operation Definition Semantic Role Proof Obligation 
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. [AL90]
    Composing Specifications. M. Abadi and L. Lamport. DEC Technical Report 66, October 1990.Google Scholar
  2. [Abrial90]
    Abstract Machines, Parts I, II and III. J. R. Abrial. Unpublished, 1990.Google Scholar
  3. [ALNS91]
    The B Method. J. R. Abrial, M. K. O. Lee, D. S. Neilson and P. N. Scharbach. VDM '91, Formal Software Development Methods, LNCS 552, Springer-Verlag (1991).Google Scholar
  4. [AhKee89]
    Operation Decomposition Proof Obligations for Blocks and Procedures. J. A. Ah-Kee. Ph.D. Thesis. University of Manchester. 1989.Google Scholar
  5. [Back88]
    A Calculus of Refinements for Program Derivations. R.J.R. Back. Acta Informatica (1988).Google Scholar
  6. [BW90]
    Duality in Specification Languages: A Lattice-theoretical Approach. R.J.R. Back and J. von Wright. Acta Informatica 27, 1990, pp 583–625.CrossRefGoogle Scholar
  7. [BR91]
    Reasoning about VDM developments using the VDM support tool in Mural. J.C. Bicarregui and B. Ritchie, in VDM '91 Formal Software Development Methods. LNCS 552, Springer-Verlag (1991).Google Scholar
  8. [BFLMR93]
    Proof in VDM — A Practitioner's Guide. J.C.Bicarregui, J.F. Fitzgerald, P.A. Lindsay, R. Moore and B. Ritchie, To appear Springer-Verlag (1993).Google Scholar
  9. [Dijkstra76]
    A Discipline of Programming. E.W.Dijkstra, Prentice-Hall (1976).Google Scholar
  10. [Jones87]
    VDM Proof Obligations and their Justification. C.B.Jones, Proceedings of the VDM '87 Symposium, LNCS 252, Springer-Verlag(1987).Google Scholar
  11. [Jones90]
    C.B.Jones, Systematic Software Development using VDM. (second edition) Prentice Hall, 1990.Google Scholar
  12. [Lamport91]
    The Temporal Logic of Actions. L. Lamport, DEC Technical Report 79. December 25, 1991.Google Scholar
  13. [Milne88]
    Proof Rules for VDM Statements. R. Milne, Proceedings of the VDM '88 Symposium, LNCS 328, Springer-Verlag(1988).Google Scholar
  14. [Morgan86]
    The Specification Statement. C. Morgan. TOPLAS 10, 3 (July 1988).Google Scholar
  15. [Morgan88]
    On the Refinement Calculus. C. Morgan, K. Robinson and P. Gardiner. Oxford University Technical Monograph, PRG-70, 1988.Google Scholar
  16. [Morgan90]
    Programming from Specifications. C. Morgan, Prentice Hall, 1990.Google Scholar
  17. [Morris87]
    A theoretical basis for stepwise refinement and the programming calculus. J. Morris, Sci.Comput. Programming, 9 287–306 (1987).CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Juan Bicarregui
    • 1
  1. 1.Systems Engineering DivisionSERC Rutherford Appleton LaboratoryOxonUK

Personalised recommendations