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).