3

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

4

5 回答 5

5

据我所知，迄今为止最强大的静态 DbC 语言是Microsoft Research 的 Spec#。它使用名为Boogie的强大静态分析工具，该工具又使用名为Z3的强大定理证明器/约束求解器来证明设计时合同的履行或违反。

If the Theorem Prover can prove that a contract will always be violated, that's a compile error. If the Theorem Prover can prove that a contract will never be violated, that's an optimization: the contract checks are removed from the final DLL.

As Charlie Martin points out, proving contracts in general is equivalent to solving the Halting Problem and thus not possible. So, there will be a lot of cases, where the Theorem Prover can neither prove nor disprove the contract. In that case, a runtime check is emitted, just like in other, less powerful contract systems.

请注意，不再开发 Spec#。合约引擎已被提取到一个名为Code Contracts for .NET的库中，它将成为 .NET 4.0 / Visual Studio 2010 的一部分。但是，合约将不提供语言支持。

于 2009-01-07T02:52:35.630 回答
1

编译器可以使用静态分析来查看您的程序并确定它是否正确。作为一个简单的示例，以下代码可能会尝试对负数 (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用负数调用。

于 2009-01-06T23:29:00.347 回答
1

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

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

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

于 2009-01-06T23:38:01.933 回答
0

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

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

  foo(a);

在其他地方定义

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

然后编译器可以检查 a 实际上是否在开区间 (0..128) 中。

于 2009-01-06T23:27:01.100 回答
0

像D这样的一些语言具有相当强大的编译时常量折叠和编译时条件检查（对于 D static assert(boolCond, msg);，IIRC C/C++ 可以使用#ifand pragmaor #error）

于 2009-01-07T00:41:46.940 回答