代码之家 › 专栏 › 技术社区 › user7860670

是否可以在编译时强制执行合同设计检查?

eiffel design-by-contract

0

user7860670 · 技术社区 · 6 年前

阅读 Design by Contract tutorial 我偶然发现了下面这句话:

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

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

1 回复 | 直到 6 年前

1

Alexander Kogtenkov 6 年前

有工具 AutoProof 用于在编译时验证合同。它执行一些转换,以一个SMT实例结束,该实例由Z3SMT解算器检查,该解算器指示是否所有断言都有效。从简报中 introduction 因此,使用它需要相当多的注释。然而,该工具被用来验证 Base2 ,一组容器类,类似于基地图书馆。合同依赖于所谓的 语义协作 相应论文中描述的技术(寻找 出版物 在自动驾驶室 page )

有一些正在进行中 research work 为了简化AutoToping使用的技术,修复现有问题,使其适应使用 void-safe 系统和 SCOOP (简单的并发面向对象编程)。截至撰写之时,该技术仍处于研究阶段,尚未准备好在生产环境中充分使用。主要障碍是使用该技术所需的复杂性和特殊培训。然而,基本的想法是相当普遍的,允许在教学过程中使用该工具。