[1] Surprisingly, this idea is very difficult to formulate rigorously. There are two approaches to giving such a formulation. One, pioneered by C. A. R. Hoare (1972), is known as the method of abstract models. It formalizes the procedures plus conditions functions plus conditions specification as outlined in the rational-number example above. Note that the condition on the rational-number representation was stated in terms of facts about integers (equality and division). In general, abstract models define new kinds of data objects in terms of previously defined types of data objects. Assertions about data objects can therefore be checked by reducing them to assertions about previously defined data objects. Another approach, introduced by Zilles at MIT, by Goguen, Thatcher, Wagner, and Wright at IBM (see Thatcher, Wagner, and Wright 1978), and by Guttag at Toronto (see Guttag 1977), is called algebraic specification. It regards the procedures functions as elements of an abstract algebraic system whose behavior is specified by axioms that correspond to our conditions, and uses the techniques of abstract algebra to check assertions about data objects. Both methods are surveyed in the paper by Liskov and Zilles (1975).
[2] The function error introduced in section 1.3.3 takes as optional second argument a string that gets displayed before the first argument—for example, if m is 42: Error in line 7: argument not 0 or 1 -- pair: 42
2.1.3   What Is Meant by Data?