TY - GEN
T1 - Contracts as Pairs of projections
AU - Findler, Robert Bruce
AU - Blume, Matthias
PY - 2006
Y1 - 2006
N2 - Assertion-based contracts provide a powerful mechanism for stating invariants at module boundaries and for enforcing them uniformly. In 2002, Findler and Felleisen showed how to add contracts to higher-order functional languages, allowing programmers to assert invariants about functions as values. Following up in 2004, Blume and McAllester provided a quotient model for contracts. Roughly speaking, their model equates a contract with the set of values that cannot violate the contract. Their studies raised interesting questions about the nature of contracts and, in particular, the nature of the any contract. In this paper, we develop a model for software contracts that follows Dana Scott's program by interpreting contracts as projections. The model has already improved our implementation of contracts. We also demonstrate how it increases our understanding of contract-oriented programming and design. In particular, our work provides a definitive answer to the questions raised by Blume and McAllester's work. The key insight from our model that resolves those questions is that a contract that puts no obligation on either party is not the same as the most permissive contract for just one of the parties.
AB - Assertion-based contracts provide a powerful mechanism for stating invariants at module boundaries and for enforcing them uniformly. In 2002, Findler and Felleisen showed how to add contracts to higher-order functional languages, allowing programmers to assert invariants about functions as values. Following up in 2004, Blume and McAllester provided a quotient model for contracts. Roughly speaking, their model equates a contract with the set of values that cannot violate the contract. Their studies raised interesting questions about the nature of contracts and, in particular, the nature of the any contract. In this paper, we develop a model for software contracts that follows Dana Scott's program by interpreting contracts as projections. The model has already improved our implementation of contracts. We also demonstrate how it increases our understanding of contract-oriented programming and design. In particular, our work provides a definitive answer to the questions raised by Blume and McAllester's work. The key insight from our model that resolves those questions is that a contract that puts no obligation on either party is not the same as the most permissive contract for just one of the parties.
UR - http://www.scopus.com/inward/record.url?scp=33745865463&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33745865463&partnerID=8YFLogxK
U2 - 10.1007/11737414_16
DO - 10.1007/11737414_16
M3 - Conference contribution
AN - SCOPUS:33745865463
SN - 3540334386
SN - 9783540334385
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 226
EP - 241
BT - Functional and Logic Programming
PB - Springer Verlag
T2 - 8th International Symposium on Functional and Logic Programming, FLOPS 2006
Y2 - 24 April 2005 through 26 April 2005
ER -