Modular set-based analysis from contracts
Modular set-based analysis from contracts
复制标题
来自合约的模块化基于集合的分析
DOI：
10.1145/1111037.1111057
复制
发表时间：
2006
影响因子：
--
通讯作者：
M. Felleisen
中科院分区：
文献类型：
--
作者：
P. Meunier;R. Findler;M. Felleisen
在PLT方案中，计划由带有合同的模块组成。后者通过谓词描述了功能和对象的输入和输出。运行时系统执行这些谓词；如果谓词失败，执行者会提出一个例外，将特定模块归咎于故障的解释。在本文中，我们展示了如何使用此类模块合同将基于设定的分析转换为完全模块化的参数化分析。使用此分析，静态调试器可以指示任何给定的合同检查是否始终满足，部分满足或（可能）完全违反相应的谓词。静态调试器还可以预测潜在错误的根源，即，对于合同制度的责备分配是正确的。
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.