Contract-oriented specifications

In object classes developed using design-by-contract, contracts contain assertions that formalise pre-conditions, post-conditions and invariants. To be sure that contracts are complete, they can be derived from specifications. For classes in a data structure library, equational specifications are appropriate. However, a conventional equational specification cannot usually be mapped directly to contracts. Instead, a second, contract-oriented, equational specification can be devised, with two key properties: it can be proved that the contract-oriented specification implies the original specification; and the contract-oriented specification can be mapped systematically to contracts. These two properties combine to increase the confidence that the contracts capture the same abstraction as the equational specification