Contract soundness for object-oriented languages

Robert Bruce Findler*, Matthias Felleisen

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

73 Scopus citations


Checking pre- and post-conditions of procedures and methods at runtime helps improve software reliability. In the procedural world, pre- and post-conditions have a straightforward interpretation. If a procedure's pre-condition doesn't hold, the caller failed to establish the proper context. If a post-condition doesn't hold, the procedure failed to compute the expected result. In the object-oriented world, checking pre- and post-conditions for methods, often called contracts in this context, poses complex problems. Because methods may be overridden, it is not sufficient to check only pre- and post-conditions. In addition, the contract hierarchy must be checked to ensure that the contracts on overriden methods are properly related to the contracts on overriding methods. Otherwise, a class hierarchy may violate the substitution 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-oriented world from a foundational perspective. More specifically, we study contracts 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.

Original languageEnglish (US)
Title of host publicationProceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA
Number of pages15
StatePublished - Dec 1 2001
EventConference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2001) - Tampa Bay, FL, United States
Duration: Oct 14 2001Oct 18 2001


OtherConference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2001)
Country/TerritoryUnited States
CityTampa Bay, FL

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Contract soundness for object-oriented languages'. Together they form a unique fingerprint.

Cite this