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

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

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

如果Theorem Prover可以证明合同总是会被违反,那就是编译错误.如果Theorem Prover可以证明合同永远不会被违反,那就是优化:合同检查从最终的DLL中删除.

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

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