Contract soundness for object-oriented languages

Citation
Rb. Findler et M. Felleisen, Contract soundness for object-oriented languages, ACM SIGPL N, 36(11), 2001, pp. 1-15
Citations number
21
Categorie Soggetti
Computer Science & Engineering
Journal title
ACM SIGPLAN NOTICES
ISSN journal
15232867 → ACNP
Volume
36
Issue
11
Year of publication
2001
Pages
1 - 15
Database
ISI
SICI code
1523-2867(200111)36:11<1:CSFOL>2.0.ZU;2-H
Abstract
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.