design-by-contract - 是否可以在编译时强制执行按合同设计的检查？

Question

阅读合同设计教程我偶然发现了以下行：

埃菲尔的合同不仅仅是一厢情愿。它们可以在编译选项的控制下在运行时进行监控。

然后解释他们在失败时会抛出异常。这让我觉得所有require ensure invariant all检查都可以在运行时执行或关闭。这个对吗？或者它们也可以在编译时使用适当的编译器选项强制执行？

标签： design-by-contracteiffel

Answer 1

有一个工具AutoProof用于在编译时验证合约。它执行一些转换，最终得到一个 SMT 实例，该实例由 Z3 SMT 求解器检查，该求解器告诉所有断言是否成立。从简要介绍中可以看出，使用它需要相当多的注释。然而，该工具用于验证Base2，一组容器类，类似于Base库的标准类。这些合同依赖于相应论文中描述的所谓的语义协作技术（在 AutoProof页面查找出版物）。

正在进行一些研究工作，以简化 AutoProof 采用的技术，修复现有问题，使其适用于void-safe系统和SCOOP（简单并发面向对象编程）。截至撰写本文时，该技术仍处于研究阶段，尚未准备好在生产环境中主要使用。主要障碍是使用该技术所需的复杂性和特殊培训。但是，基本思想非常笼统，可以在教学过程中使用该工具。