Modular set-based analysis from contracts

Philippe Meunier*, Robert Bruce Findler, Matthias Felleisen

*Corresponding author for this work

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

17 Scopus citations

Abstract

In PLT Scheme, programs consist of modules with contracts. The latter describe the inputs and outputs of functions and objects via predicates. A run-time system enforces these predicates; if a predicate fails, the enforcer raises an exception that blames a specific module with an explanation of the fault. In this paper, we show how to use such module contracts to turn set-based analysis into a fully modular parameterized analysis. Using this analysis, a static debugger can indicate for any given contract check whether the corresponding predicate is always satisfied, partially satisfied, or (potentially) completely violated. The static debugger can also predict the source of potential errors, i.e., it is sound with respect to the blame assignment of the contract system.

Original languageEnglish (US)
Title of host publicationConference Record of POPL 2006
Subtitle of host publication33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
PublisherAssociation for Computing Machinery
Pages218-231
Number of pages14
ISBN (Print)1595930272, 9781595930279
DOIs
StatePublished - 2006
Event33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'06 - Charleston, SC, United States
Duration: Jan 11 2006Jan 13 2006

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566

Conference

Conference33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'06
Country/TerritoryUnited States
CityCharleston, SC
Period1/11/061/13/06

Keywords

  • Modular Analysis
  • Runtime Contracts
  • Set-based Analysis
  • Static Debugging

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Modular set-based analysis from contracts'. Together they form a unique fingerprint.

Cite this