Paper Info
Title
Complete monitors for behavioral contracts
Abstract
A behavioral contract in a higher-order language may invoke methods of unknown objects. Although this expressive power allows programmers to formulate sophisticated contracts, it also poses a problem for language designers. Indeed, two distinct semantics have emerged for such method calls, dubbed lax and picky. While lax fails to protect components in certain scenarios, picky may blame an uninvolved party for a contract violation. In this paper, we present complete monitoring as the fundamental correctness criterion for contract systems. It demands correct blame assignment as well as complete monitoring of all channels of communication between components. According to this criterion, lax and picky are indeed incorrect ways to monitor contracts. A third semantics, dubbed indy, emerges as the only correct variant.
Year
DOI
Venue
2012
10.1007/978-3-642-28869-2_11
ESOP
Keywords
DocType
Volume
higher-order language,distinct semantics,fundamental correctness criterion,correct blame assignment,contract violation,sophisticated contract,correct variant,contract system,complete monitoring,behavioral contract
Conference
7211
ISSN
Citations 
PageRank 
0302-9743
20
0.67
References 
Authors
7
3
Name
Order
Citations
PageRank
Christos Dimoulas1966.44
Sam Tobin-Hochstadt239124.82
Matthias Felleisen33001272.57