Object-oriented Programming Languages Need Well-founded Contracts

Over the past few years, the notion of building software from components has become popular again. The goal is to produce systems by adapting and linking off-the-shelf modules from a pool of interchangeable components. To turn this idea into reality, the formal descriptions of software components need to specify more than the type signatures of their exported services. At a minimum, they should contain assertions about critical properties of a component's behavior. By monitoring such behavioral contracts at run-time, language implementations can pinpoint faulty components, and programmers can replace them with different ones. In this paper, we study the notion of behavioral contracts in an object-oriented setting. While the use of behavioral contracts is well-understood in the world of procedural languages, their addition to object-oriented programming languages poses remarkably subtle problems. All existing contract enforcement tools for Java fail to catch flaws in contracts or blame the wrong component for contractual violations. The failures point to a lack of foundational research on behavioral contracts in the OOP world