Issue No. 02 - February (1995 vol. 21)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.345824
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 nondeterminism and increase in definedness. This paper makes a comparison of the two notations through an example of a communications protocol previously formalized in [<ref type="bib" rid="S00791">1</ref>]. 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 generalized substitutions.
Abstract Machine Notation, B, formal methods, model-oriented specification, VDM
J. Bicarregui and B. Ritchie, "Invariants, Frames and Postconditions: A Comparison of the VDM and B Notations," in IEEE Transactions on Software Engineering, vol. 21, no. , pp. 79-89, 1995.