在合同设计中编译时间检查？

StackOverflow https://stackoverflow.com/questions/418588

  •  03-07-2019
  •  | 
  •  

题

我读过编译器可以在编译时强制执行dbc ..它是如何实现的？

有帮助吗？

解决方案

据我所知，迄今为止最强大的静态DbC语言是 Microsoft Research的Spec＃。它使用一个强大的静态分析工具 Boogie ，后者又使用强大的定理证明器/约束解算器< a href =“http://Research.Microsoft.Com/projects/z3/”rel =“noreferrer”> Z3 ，以证明在设计时履行或违反合同。

如果Theorem Prover可以证明合同将总是被违反，那就是编译错误。如果Theorem Prover可以证明合同将永远违反，那就是优化：合同检查将从最终的DLL中删除。

正如查理·马丁所指出的那样，证明合同总体上等同于解决停机问题，因此不可能。因此，会有很多案例，定理证明者既不能证明也不反驳合同。在这种情况下，会发出运行时检查，就像在其他功能较弱的合同系统中一样。

请注意，不再开发Spec＃。合同引擎已被提取到一个名为 .NET代码合同的库中，该库将成为其中的一部分.NET 4.0 / Visual Studio 2010.但是，合同没有语言支持。

其他提示

编译器可以使用静态分析查看您的程序并确定它是否执行正确的事。举个简单的例子，下面的代码可能会尝试取负数的平方根（C ++）：

double x;
cin >> x;
cout << sqrt(x) << endl;

如果编译器知道永远不应该用负数调用 sqrt ，它可能会将此标记为问题，因为它知道从用户输入读取可以返回负数。另一方面，如果你这样做：

double x;
cin >> x;
if (x >= 0) {
    cout << sqrt(x) << endl;
} else {
    cout << "Can't take square root of negative number" << endl;
}

然后编译器可以告诉该代码不会使用负数调用 sqrt 。

契约式设计是一个非常抽象的术语，因为可以有许多具有不同表达能力的规范形式。此外，目前对静态分析检查和实施规范的能力存在限制。它是计算机科学领域最活跃的学术和工业研究领域之一。

实际上，您可能会使用某些合同和检查子集，这取决于您使用的语言以及您安装的插件或程序。

通常，静态分析会尝试构建合同模型和实际程序的模型，并进行比较。例如，如果合约不允许您在对象处于状态S时调用函数，它将尝试确定在任何调用序列中是否可以最终处于状态S.

哪种编译器和什么语言？埃菲尔在某种程度上可以做到。但请记住，完全强制执行按合同设计意味着能够解决停机问题（证明：假设您有一个可以执行此操作的编译器。那么编译器必须能够识别具有真实退出条件的任意函数由于无限循环或无限递归而无法实现退出条件。因此它会减少为停止。）

这通常意味着如果你有一个电话

  foo(a);

以及其他地方定义

  function foo(a:int) is
     assert 0 < a && a < 128
     ...
  end

然后编译器可以检查a实际上是否处于开放区间（0..128）。

D 等某些语言具有相当强大的编译时常量折叠和编译时条件检查（适用于D 静态断言（boolCond，msg）; ，IIRC C / C ++可以使用 #if 和 pragma 或 #error ）

许可以下： CC-BY-SA 和 归因
不隶属于 StackOverflow
scroll top