静态合同简化
Static Contract Simplification
摘要：
契约和契约监视是指定属性并在运行时间保证它们的强大机制。然而，契约的运行时间监视强加了显著的开销。执行时间受到插入合约检查以及引入代理对象（按需执行延迟合约检查）的影响。静态契约简化使用程序转换来解决这个问题。它将编译时转换应用于具有契约的程序，以减少总体运行时间，同时保留原始行为。我们的关键技术是通过程序静态传播合同，并在可能的情况下评估和合并合同。我们的目标是获得剩余的契约，这些契约在运行时间检查起来更便宜。我们区分不同层次的行为保护，这对可接受的转换施加了不同的限制：强责任保护，转换是一个行为等价，和弱责任保护，转换后的程序相当于特定的违规报告。我们的转换从未增加合同检查的总数。
英文摘要：
Contracts and contract monitoring are a powerful mechanism for specifying properties and guaranteeing them at run time. However, run time monitoring of contracts imposes a significant overhead. The execution time is impacted by the insertion of contract checks as well as by the introduction of proxy objects that perform delayed contract checks on demand. Static contract simplification attacks this issue using program transformation. It applies compile-time transformations to programs with contracts to reduce the overall run time while preserving the original behavior. Our key technique is to statically propagate contracts through the program and to evaluate and merge contracts where possible. The goal is to obtain residual contracts that are collectively cheaper to check at run time. We distinguish different levels of preservation of behavior, which impose different limitations on the admissible transformations: Strong blame preservation, where the transformation is a behavioral equivalence, and weak blame preservation, where the transformed program is equivalent up to the particular violation reported. Our transformations never increase the overall number of contract checks.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
