Modular set-based analysis from contracts

11 years 1 months ago
Modular set-based analysis from contracts
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. Categories and Subject Descriptors F.3.2 [Semantics of Programming Languages]: Program analysis; D.2.4 [Software / Program Verification]: Programming by contract General Terms Languages, Reliability, Verification. Keywo...
Philippe Meunier, Robert Bruce Findler, Matthias F
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2006
Where POPL
Authors Philippe Meunier, Robert Bruce Findler, Matthias Felleisen
Comments (0)