ePubs

The open archive for STFC research publications

Full Record Details

Persistent URL http://purl.org/net/epubs/work/28875
Record Status Checked
Record Id 28875
Title Invariants, Frames and Postconditions: A Comparison of the VDM and B Notations
Contributors
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 [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 generalised substitutions.
Organisation CCLRC , BITD
Keywords
Funding Information
Related Research Object(s):
Licence Information:
Language English (EN)
Type Details URI(s) Local file(s) Year
Paper In Conference Proceedings In Industrial-Strength Formal Methods - Proceeding of Formal Methods Europe '93 (FME 93), Odense, Denmark, 19-23 April, 1993, (1995). 10.1.1.39.4792.pdf 1995