按合同设计中的编译时间检查? [英] Compile time checking in Design by Contract?

问题描述

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

I read that compiler can enforce dbc at compile time.. How does it do it?

推荐答案

据我所知，到目前为止，最强大的静态DbC语言是规范由Microsoft Research提供.它使用了称为 Boogie 的强大静态分析工具，该工具反过来又使用了称为 Z3 以在设计时证明合同的履行或违反.

As far as I know, the most powerful static DbC language so far is Spec# by Microsoft Research. It uses a powerful static analysis tool called Boogie which in turn uses a powerful Theorem Prover / Constraint Solver called Z3 to prove either the fulfillment or violation of contracts at design time.

如果定理证明者可以证明合同将始终被违反，那就是编译错误.如果定理证明者能够证明合同将永远不会被违反，那就是一种优化:将合同检查从最终的DLL中删除.

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.

正如查理·马丁(Charlie Martin)指出的那样，证明合同总体上等同于解决停止问题，因此是不可能的.因此，在很多情况下，定理证明者无法证明或反驳合同.在这种情况下，就像在其他功能较弱的合同系统中一样，将发出运行时检查.

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#.合同引擎已提取到名为 .NET的代码合同的库中，该库将是其中的一部分.NET 4.0/Visual Studio 2010的版本.但是，合同不支持任何语言.

Please note that Spec# is no longer being developed. The contract engine has been extracted into a library, called Code Contracts for .NET, which will be a part of .NET 4.0 / Visual Studio 2010. However, there will be no language support for contracts.

这篇关于按合同设计中的编译时间检查?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！