TY - JOUR
T1 - Contract soundness for object-oriented languages
AU - Findler, Robert
AU - Felleisen, Matthias
N1 - Funding Information:
Thanks to Philippe Meunier for his detailed comments on a draft of this paper. We also thank Daniel Jackson, Shriram Krishnamurthi, and Clemens Szyperski for valuable discussionsabout this work. In addition, we gratefully acknowledge the support of the NSF (CCR-9619756) and Texas ATP (#003604-0126-1999).
Funding Information:
Thanks to Philippe Meunier for his detailed comments on a draft of this paper. We also thank Daniel Jackson, Shriram Krishnamurthi, and Clemens Szyperski for valuable discussions about this work. In addition, we gratefully acknowledge the support of the NSF (CCR-9619756) and Texas ATP (#003604-0126-1999).
Publisher Copyright:
© ACM 2001
PY - 2011/11/1
Y1 - 2011/11/1
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85062226787&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85062226787&partnerID=8YFLogxK
U2 - 10.1145/504311.504283
DO - 10.1145/504311.504283
M3 - Article
AN - SCOPUS:85062226787
VL - 36
SP - 1
EP - 15
JO - ACM SIGPLAN Notices
JF - ACM SIGPLAN Notices
SN - 1523-2867
IS - 11
ER -