据我所知，迄今为止最强大的静态设计通过约束语言为微软研究开发的Spec#。 它使用一个名为Boogie的强大静态分析工具，该工具反过来使用一个名为Z3的强大定理证明/约束求解器，在设计时证明合同的履行或违反。

如果定理证明器能够证明一个合约总是会被违反，那就是编译错误。如果定理证明器能够证明一个合约永远不会被违反，那就是一种优化：合约检查被从最终的DLL中移除了。

正如Charlie Martin所指出的那样，通常证明合同等价于解决停机问题，因此是不可能的。因此，会有很多情况，Theorem Prover既不能证明也不能推翻合同。在这种情况下，会发出运行时检查，就像其他不那么强大的合同系统一样。

请注意，Spec＃不再被开发。合同引擎已提取到名为.NET的库中，称为.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。

哪种编译器和哪种语言？Eiffel在某种程度上可以做到这一点。但要记住，完全强制实施契约设计意味着能够解决停机问题（证明：假设您有一个可以完成此操作的编译器。那么编译器必须能够识别具有真正的退出条件的任意函数，该函数由于无限循环或无限递归而无法达到退出条件。因此它降低到了停机。）

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

  foo(a);

请翻译成中文：“and somewhere else define” 并在其他地方定义。

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

然后编译器可以检查a实际上将在开区间（0..128）中。

有些语言，比如D，具有相当强的编译时常量折叠和编译时条件检查功能（对于D来说，有static assert(boolCond, msg);，如果我没有记错，C/C++可以使用#if和pragma或#error）。