The idea of
model-based specifications builds on two seminal papers by Hoare.
Hoare's paper ``An Axiomatic Basis for Computer Programming'' [19],
used two predicates over program states to specify a computation.
The first predicate specifies the requirements on the state before the
computation; it is called the computation's
*precondition*.
The second predicate specifies the desired final state;
it is called the computation's *postcondition*.

Hoare's paper ``Proof of correctness of data representations'' [20],
described the verification of abstract data type (ADT)
implementations.
In this paper Hoare introduced the use of
an abstraction function that maps
the implementation data structure (e.g., an array) to a mathematical
value space (e.g., a set).
The elements of this value space are thus called *abstract values*
[35].
The idea is that one specifies the ADT using the abstract values,
which allows clients of the ADT's operations to reason about calls
without worrying about the details of the implementation.

A *model-based* specification language combines these
ideas. That is, it specifies procedures (what C++ calls functions),
using pre- and postconditions.
The pre- and postconditions use the vocabulary
specified in an *abstract model*,
which specifies the abstract values mathematically.

The best-known model-based specification languages are VDM-SL [21] and Z [44,43,17]. Both come with a mathematical toolkit from which a user can assemble abstract models for use in specifying procedures. The toolkit of VDM-SL resembles that of a (functional) programming language; it provides certain basic types (integers, booleans, characters), and structured types such as records, Cartesian products, disjoint unions, and sets. The toolkit in Z is based on set theory; it has a relatively elaborate notation for various set constructions, as well as powerful techniques for combining specifications (the schema calculus).

1999-01-26