Component-based software manufacturing has the potential to
bring division-of-labor benefits to the world of software
engineering. In order to make a market of software
components viable, however, producers and consumers must
agree on enforceable software contracts and a system for
assigning blame to components that violate the contracts.
This dissertation explores pre- and post-condition, run-time
enforced behavioral contracts. The dissertation makes three
contributions:
Existing object-oriented contract checking systems
incorrectly enforce contracts in the presence of
subtyping. They may mis-assign blame for contract
violations or even ignore contract violations. This
dissertation explains how these contract checkers fail and
shows how to properly check contracts in these situations.
Previously, languages with first-class functions could not
benefit from pre- and post-condition-style contracts. This
dissertation shows how to enforce pre- and post-condition
style contracts on first-class functions and correctly
assign blame for such contract violations.
Finally, this dissertation lays the groundwork for a new
theory of contract checking, in the spirit of the theory
for type checking. In particular, it states and proves the
first contract soundness result, guaranteeing that the
contract checker properly enforces contracts and properly
assigns blame for contract violations.
![[RiceCS]](http://www.cs.rice.edu/Database/media/CSLogo.gif){kind=small}
![[Rice]](http://www.cs.rice.edu/Database/media/Owl.gif){kind=small}
