TY - GEN
T1 - Option contracts
AU - Dimoulas, Christos
AU - Findler, Robert Bruce
AU - Felleisen, Matthias
N1 - Copyright:
Copyright 2013 Elsevier B.V., All rights reserved.
PY - 2013
Y1 - 2013
N2 - Many languages support behavioral software contracts so that programmers can describe a component's obligations and promises via logical assertions in its interface. The contract system monitors program execution, checks whether the assertions hold, and, if not, blames the guilty component. Pinning down the violator gets the debugging process started in the right direction. Quality contracts impose a serious runtime cost, however, and programmers therefore compromise in many ways. Some turn off contracts for deployment, but then contracts and code quickly get out of sync during maintenance. Others test contracts randomly or probabilistically. In all cases, programmers have to cope with lack of blame information when the program eventually fails. In response, we propose option contracts as an addition to the contract tool box. Our key insight is that in ordinary contract systems, server components impose their contract on client components, giving them no choice whether to trust the server's promises or check them. With option contracts, server components may choose to tag a contract as an option and clients may choose to exercise the option or accept it, in which case they also shoulder some responsibility. We show that option contracts permit programmers to specify flexible checking policies, that their cost is reasonable, and that they satisfy a complete monitoring theorem.
AB - Many languages support behavioral software contracts so that programmers can describe a component's obligations and promises via logical assertions in its interface. The contract system monitors program execution, checks whether the assertions hold, and, if not, blames the guilty component. Pinning down the violator gets the debugging process started in the right direction. Quality contracts impose a serious runtime cost, however, and programmers therefore compromise in many ways. Some turn off contracts for deployment, but then contracts and code quickly get out of sync during maintenance. Others test contracts randomly or probabilistically. In all cases, programmers have to cope with lack of blame information when the program eventually fails. In response, we propose option contracts as an addition to the contract tool box. Our key insight is that in ordinary contract systems, server components impose their contract on client components, giving them no choice whether to trust the server's promises or check them. With option contracts, server components may choose to tag a contract as an option and clients may choose to exercise the option or accept it, in which case they also shoulder some responsibility. We show that option contracts permit programmers to specify flexible checking policies, that their cost is reasonable, and that they satisfy a complete monitoring theorem.
KW - Behavioral software contracts
KW - Probabilistic spot checking
KW - Programming language design
KW - Random testing
UR - http://www.scopus.com/inward/record.url?scp=84888194953&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84888194953&partnerID=8YFLogxK
U2 - 10.1145/2509136.2509548
DO - 10.1145/2509136.2509548
M3 - Conference contribution
AN - SCOPUS:84888194953
SN - 9781450323741
T3 - Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA
SP - 475
EP - 494
BT - SPLASH Indianapolis 2013
T2 - 2013 28th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2013
Y2 - 29 October 2013 through 31 October 2013
ER -