 Axiomatic specification

Describe operations through laws relating their observable results, without selecting an internal representation. For an abstract data type, the laws must state the operation domains and error results as well as ordinary cases. A disjoint union can distinguish a successful value from an error with the same textual spelling.