Advertisement

Invariants, frames and postconditions: a comparison of the VDM and B notations

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

Abstract

VDM and B are two “model-oriented” formal methods. Each gives a notation for the specification of systems as state machines in terms of a set of states with operations defined as relations on that set. Each has a notion of refinement of data and operations based on the principles of reduction of non-determinism and increase in definedness.

This paper makes a comparison of the two notations through an example of a communications protocol previously formalised in [BA91]. Two abstractions and two reifications of the original specification are given. Particular attention is paid to three areas where the notations differ: the use of postconditions that assume the invariant as opposed to postconditions that enforce it; the explicit “framing” of operations as opposed to the “minimal frame” approach; and the use of relational postconditions as opposed to generalised substitutions.

Keywords

Operation Definition Generalise Substitution External Behaviour Abstract Specification Coupling Relation 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Abrial92a]
    Abrial, J.R. Introducing B-Technologies (draft). May 1992.Google Scholar
  2. [Abrial92b]
    Abrial, J.R. The B Method. Book to appearGoogle Scholar
  3. [BA91]
    Bruns, G. and Anderson, S., The Formalisation of a Communications Protocol. LFCS Tech. Rep. 91–137 (April 1991).Google Scholar
  4. [BA92]
    Bruns, G. and Anderson, S., The Formalization of a Communications Protocol. LFCS/Adelard SCCS Tech.Rep. April 6, 1992.Google Scholar
  5. [Bicarregui93]
    Bicarregui, J.C. Algorithm refinement with read and write frames, In this volume.Google Scholar
  6. [BR93]
    Bicarregui, J.C. and B. Ritchie. A Comparison of Two Formal Specification Notations, RAL Technical Report, 1993.Google Scholar
  7. [Jones90]
    Jones, C.B. Systematic Software Development Using VDM, second edition. Prentice Hall, 1990.Google Scholar
  8. [Morgan91]
    Morgan, C. Programming from Specifications. Prentice Hall, 1990.Google Scholar
  9. [Santoline89]
    L.L. Santoline et al. Multiprocessor Shared-Memory Information Exchange. IEEE Trans. on Nuclear Science. 36(1) 1989, pp.626–633.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

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

Personalised recommendations