Sciweavers

Share
ESOP
2012
Springer

Complete Monitors for Behavioral Contracts

8 years 3 months ago
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.
Christos Dimoulas, Sam Tobin-Hochstadt, Matthias F
Added 21 Apr 2012
Updated 21 Apr 2012
Type Journal
Year 2012
Where ESOP
Authors Christos Dimoulas, Sam Tobin-Hochstadt, Matthias Felleisen
Comments (0)
books