To achieve the next level of software productivity, programs should consist of off-the-shelf, interchangeable components that are produced by a network of independent software companies. In turn, programming languages will need to provide sub-languages for formulating independent components and enforceable contracts between them. Component sublanguages have received plenty of attention over the past few years with the development of rich module systems. As for contracts, language researchers have almost exclusively focused on types, which excludes properties that can only be checked at run-time.
Eiffel and iContract (a Java dialect) are related attempts to address this problem. They incorporate a notion of checkable contract. A contract consists of pre- and post-conditions on individual methods. Unfortunately, both systems blame the wrong component when objects are used as first-class data, an increasingly common programming style. At best, this misplaced blame misleads the programmer in his search for bugs; at worst, it destroys a company for the wrong reason.
In response to these failures, we are developing a semantic framework for components and contracts. My talk will describe two contributions. The first is a mechanism for assigning meaning to contracts. Specifically, I will present a calculus of Scheme with components and contracts. Roughly speaking, a component is a module with external links, and a contract is a predicate type, including predicates that can only be checked at run-time. The calculus determines what it means for values to cross component boundaries and for a component to break its contract. The second contribution is an example of how one can use the semantic framework to prove a contract compiler correct. The compiler inserts run-time checks and module source information based on the contracts. The correctness theorem shows that, if a run-time check raises an exception, its error message blames the unit to which the calculus assigns responsibility.
Joint work with: Robby B. Findler