Summary of Set-theoretic Specifications (tentative)

CS

Set-theoretic specifications, which are also knows as "model-based specifications" or "model-oriented specifications" , model systems using sets which are either considered to be primitives sets or constructed by means of combinations of primitive subsets using set-theoretic operations. Specific languages can be distinguished from each other according to the way set-theoretic concepts are used, their underlying-logic or how they assist in the production of programs from specifications. Here, some well-known formal notations representative of the approach Z, which appeared in the 1970s, VDM, which was born in the 1960s, and B, which was developed in the 1990s.

VDM (Vienna Development Method) Z-notation B-method
born in 1978 1977 1990s
Early Develoment By Bjørner Dines and Cliff B. Jones in IBM's Vienna Laboratory Jean-Raymond Abrial Jean-Raymond Abrial, et al
Specification laguage VDM-SL, VDM++ Z-notation AbstractMachine Notation (AMN)
Underlying Logic/theory Set Theory & three-valued logic Set Theory (Zermelo-Fraenkel set theory) Set Theory
Featurse of specification style pre, post condition pre, post Abrial's Generalised Substitution Language (GSL) (an extension of Dijkstra's guarded commands)
proof objects Consistency checking of redundant description of pre/post conditions and invariants check of the weakest preconditions check of the weakest preconditions generated using explicitly noted invariants
emphasis on computer aided verification and animation (rather than documentation) documentation (as the word "notation" represents) computer aided verification and animation (rather than documentation)
code readability ○ ◎ ○
tool support ◎(rich) ○ ○
advantages readable specifications
disadvantages treating concurrency modularity is clumsy treating concurrency is clumsy, the toolset for Z is still not very advanced by industrial standards.
  • Underlying Proof theory/techniques of specification correctness.

Z-notation, VDM and B-methods achieve correctness in a quite similar way, i.e., by proof using the notion of pre/post-conditions and invariants. But they each have a different treatment of pre/post-condition and invariants.

    • VDM, In VDM the preconditions are explicit. The redundant act of explicitly stating a precondition allows consistency checking: is the real precondition of the operation covered by the stated one?
    • Z-notation : In Z, the precondition is not explicitly stated; it, more exactly weakest precondition, has to be calculated from the delta schema definitions.
    • B-method, in B-method the preconditions are explicit. The redundant act of explicitly stating a precondition allows consistency checking: is the real precondition of the operation covered by the stated one? Moreover,