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