The Community for Technology Leaders
Green Image
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.
82 ms
(Ver 3.3 (11022016))