This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Invariants, Frames and Postconditions: A Comparison of the VDM and B Notations
February 1995 (vol. 21 no. 2)
pp. 79-89
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 [1]. 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.

[1] G. Bruns and S. Anderson,“The formalization and analysis of a communications protocol,”Formal Aspects of Computing,vol. 6, pp. 92–112, 1994; (Previously released as“The formalization of a communications protocol,”University of Edinburgh Tech. Rep. LFCS 91-137, April 1991, and as LFCS/Adelard SCCS Tech. Rep. April 6, 1992.
[2] C. B. Jones,Systematic Software Development Using VDM. Englewood Cliffs, NJ: Prentice-Hall, 1990, 2nd ed.
[3] J.-R. Abrial, "Assigning Programs to Meanings," Mathematical Logic and Programming Languages, Philosophical Trans. Royal Society, series A, vol. 312, 1984.
[4] L. L. Santolineet al.,“Multiprocessor shared-memory information exchange,”IEEE Trans. Nuclear Science,vol. 36, pp. 626–633, 1989.
[5] J. C. Bicarregui and B. Ritchie,“Invariants, frames and postconditions: A comparison of two formal specification notations,”Rutherford Appleton Laboratory Tech. Rep. RAL-93-100, 1993.
[6] J. R. Abrial,Introducing B-Technologies.Unpublished, May 1992.
[7] C. Morgan, Programming from Specifications, Prentice Hall, 1990.
[8] J. C. Bicarregui,“Algorithm refinement with read and write frames,”inFME'93: Industrial Strength Formal Methods, Lecture Notes in Computer Science 670,J. C. P. Woodcock and P. G. Larsen, Eds. New York: Springer-Verlag, 1993.
[9] ——,“Operation semantics with read and write frames,”inProc. BCS FACS 6th Refinement Workshop,City University, London, Jan. 5–7, 1994. To appear inWorkshops in Computing, New York: Springer-Verlag.

Index Terms:
Abstract Machine Notation, B, formal methods, model-oriented specification, VDM
Citation:
Juan Bicarregui, Brian Ritchie, "Invariants, Frames and Postconditions: A Comparison of the VDM and B Notations," IEEE Transactions on Software Engineering, vol. 21, no. 2, pp. 79-89, Feb. 1995, doi:10.1109/32.345824
Usage of this product signifies your acceptance of the Terms of Use.