Contract soundness for object-oriented languages

Robert Findler, Matthias Felleisen

Research output: Contribution to journalArticlepeer-review

1 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 overridden 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)
Pages (from-to)1-15
Number of pages15
JournalACM SIGPLAN Notices
Issue number11
StatePublished - Nov 1 2011

ASJC Scopus subject areas

  • Computer Science(all)


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

Cite this