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.
Keywords
Supported in part by AFOSR grant FA9550-09-1-0110 and the DARPA CRASH program.
References
Blume, M., McAllester, D.: Sound and complete models of contracts. Journal of Functional Programming 16(4-5), 375–414 (2006)
Dimoulas, C., Felleisen, M.: On contract satisfaction in a higher-order world. ACM Transactions on Programming Languages and Systems (TOPLAS) 33(5), 16:1 – 16:29 (2011)
Dimoulas, C., Findler, R.B., Flanagan, C., Felleisen, M.: Correct blame for contracts: No more scapegoating. In: POPL, pp. 215 – 226 (2011)
Findler, R.B., Felleisen, M.: Contracts for higher-order functions. In: ICFP, pp. 48–59 (2002)
Flatt, M.: PLT: Reference: Racket. Tech. Rep. PLT-TR-2010-1, PLT Inc. (2010), http://racket-lang.org/tr1/
Greenberg, M., Pierce, B.C., Weirich, S.: Contracts made manifest. In: POPL, pp. 353–364 (2010)
Meyer, B.: Eiffel: The Language. Prentice Hall (1992)
Tobin-Hochstadt, S., Felleisen, M.: Interlanguage migration: from scripts to programs. In: DLS, pp. 964–974 (2006)
Wadler, P., Findler, R.B.: Well-Typed Programs Can’t Be Blamed. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 1–16. Springer, Heidelberg (2009)
Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115(1), 38–94 (1994)
Zdancewic, S., Grossman, D., Morrisett, G.: Principals in programming languages: A syntactic proof technique. In: ICFP, pp. 197–207 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dimoulas, C., Tobin-Hochstadt, S., Felleisen, M. (2012). Complete Monitors for Behavioral Contracts. In: Seidl, H. (eds) Programming Languages and Systems. ESOP 2012. Lecture Notes in Computer Science, vol 7211. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28869-2_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-28869-2_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28868-5
Online ISBN: 978-3-642-28869-2
eBook Packages: Computer ScienceComputer Science (R0)