Complete monitors for behavioral contracts

Christos Dimoulas*, Sam Tobin-Hochstadt, Matthias Felleisen

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

13 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings
Pages214-233
Number of pages20
DOIs
StatePublished - 2012
Event21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012 - Tallinn, Estonia
Duration: Mar 24 2012Apr 1 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7211 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012
CountryEstonia
CityTallinn
Period3/24/124/1/12

Keywords

  • behavioral contracts
  • contract checking
  • higher-order programming

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Complete monitors for behavioral contracts'. Together they form a unique fingerprint.

Cite this