ePubs

The open archive for STFC research publications

Full Record Details

Persistent URL http://purl.org/net/epubs/work/25596
Record Status Checked
Record Id 25596
Title Invariants, Frames and Post Conditions: A Comparison of Two Formal Specification 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 [BA91. Two abstractions and two reifications of the original specification are given. Particular attention is paid to three areas where the notations differ: to the use of postconditions that assume the invariant as opposed to postconditions that enforce it; to the explicit "framing" of operations as opposed to the "minimal frame" approach; and to the use of relational postconditions as opposed to generalised substitutions.
Organisation SERC
Keywords
Funding Information
Related Research Object(s):
Licence Information:
Language English (EN)
Type Details URI(s) Local file(s) Year
Report RAL Technical Reports RAL-93-100. 1993. RAL-TR-1993-100.pdf 1993