Checking pre- and post-conditions of procedures and methods at runtime help
s improve software reliability. In the procedural world, pre- and post-cond
itions have a straightforward interpretation. If a procedure's pre-conditio
n doesn't hold, the caller failed to establish the proper context. If a pos
t-condition doesn't hold, the procedure failed to compute the expected resu
lt.
In the object-oriented world, checking pre- and post-conditions for methods
, often called contracts in this context, poses complex problems. Because m
ethods may be overridden, it is not sufficient to check only pre- and post-
conditions. In addition, the contract hierarchy must be checked to ensure t
hat the contracts on overridden methods are properly related to the contrac
ts on overriding methods. Otherwise, a class hierarchy may violate the subs
titution principle, that is, it may no longer be true that an instance of a
class is substitutable for objects of the super-class.
In this paper, we study the problem of contract enforcement in an object-or
iented world from a foundational perspective. More specifically, we study c
ontracts as refinements of types. Pushing the analogy further, we state and
prove a contract soundness theorem that captures the essential properties
of contract enforcement. We use the theorem to illustrate how most existing
tools suffer from a fundamental flaw and how they can be improved.