design-by-contract - 契约(Contract)设计中的编译时间检查？

Question

我读到编译器可以在编译时强制执行 dbc。它是怎么做到的？

Answer 1

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

如果 Theorem Prover 可以证明契约(Contract)将总是被违反，那就是编译错误。如果 Theorem Prover 可以证明契约永远不会被违反，那就是一种优化:契约检查从最终的 DLL 中移除。

正如 Charlie Martin 所指出的，证明契约(Contract)一般等同于解决停机问题，因此是不可能的。所以，在很多情况下，Theorem Prover 既不能证明也不能反驳合约。在这种情况下，会发出运行时检查，就像在其他功能较弱的契约(Contract)系统中一样。

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