【发布时间】：2018-12-09 18:34:54
【问题描述】：
阅读Design by Contract tutorial我偶然发现了以下行：
埃菲尔的合同不仅仅是一厢情愿。它们可以在编译选项的控制下在运行时进行监控。
随后解释了它们在失败时会抛出异常。这让我觉得所有的 require ensure invariant all 检查可以在运行时执行或关闭。它是否正确？或者它们也可以在编译时使用适当的编译器选项强制执行？
【问题讨论】：
【发布时间】：2018-12-09 18:34:54
【问题描述】：
有一个工具AutoProof 用于在编译时验证合约。它执行一些转换，最终得到一个 SMT 实例，该实例由 Z3 SMT 求解器检查，该求解器告诉所有断言是否成立。从简短的introduction 可以看出，使用它需要相当多的注释。然而，该工具用于验证Base2，一组容器类，类似于 Base 库的标准类。合同依赖于相应论文中描述的所谓语义协作技术（在 AutoProof page 中查找 Publications）。
有一些正在进行的research work 以简化 AutoProof 采用的技术，修复现有问题，使其适用于void-safe 系统和SCOOP（简单并发面向对象编程）。截至撰写本文时，该技术仍处于研究阶段，尚未准备好在生产环境中主要使用。主要障碍是使用该技术所需的复杂性和特殊培训。但是，基本思想非常笼统，可以在教学过程中使用该工具。
【讨论】：