Software Contracts in a Higher-order World
Abstract
The research project investigated foundational models of contracts in a higher-order world of programming. The primary thrust of the work explored the meaning of contracts. We focused on three questions. First, we determined what it means for a first-class function or object to satisfy a contract. Second, we worked out when it is correct for a contract monitoring system to blame a component for violating a contract. We could show that existing contract systems may point to an innocent component and thus send a programmer on a wild goose chase. Third, we established criteria for the completeness of monitoring systems. Using a model, we were able to demonstrate the completeness of one semantics for contract monitors. We used our primary model to explore designs for the parallel execution of contracts but without reaching a truly satisfactory answer. The secondary research project explored affine type systems as "protocol contracts" and the use of behavioral contracts to connect an affine code base to libraries from conventional languages. The result of this work is a design for a practical, ML-style programming language with an affine type system and with a contract-based mechanism for integrating existing libraries.
Document Details
- Document Type
- Technical Report
- Publication Date
- Feb 01, 2012
- Accession Number
- ADA567066
Entities
People
- Matthias Felleisen
Organizations
- Northeastern University