code-contracts - 对契约式设计或代码契约式的看法

Question

我目前正在阅读以了解有关按合同设计/代码合同的更多信息。

据我所知，它是编写合约（不变量，前置条件和后置条件）以确保代码可以保持有序。它还将保证通过基于检查和平衡的明确机制来防止错误

但这不会影响软件性能吗？因为每个方法调用之间都有额外的检查。

我非常感谢人们与我分享他们对按合同设计的观点和经验。欢迎提出缺点或优点。

Answer 1

通常，此类框架支持运行时检查和静态分析。后者在编译时（或之前）执行；它根本不会减慢您的代码速度。前者可能会影响性能。

Microsoft Research Code Contracts项目就是一个很好的例子。您可以这样配置您的系统：

• 静态分析在编译时或什至在 deigner 环境中应用可能的合同执行的一个子集；

• 对在调试模式下编译的所有代码启用运行时检查；和

• 为在发布模式下编译的代码的公共 API 启用了运行时检查的子集（非公共代码没有运行时检查）。

这通常是性能和鲁棒性之间的良好折衷。

Answer 2

应用按合同设计理念的一种方法是纯静态的。考虑一个函数的合约max_element()：

/*@
requires IsValidRange(a, n);
assigns \nothing;
behavior empty:
assumes n == 0; ensures \result == 0;
behavior not_empty:
assumes 0 < n;
ensures 0 <= \result < n;
ensures \forall integer i; 0 <= i < n ==> a[i] <= a[\result]; ensures \forall integer i; 0 <= i < \result ==> a[i] < a[\result];
complete behaviors;
disjoint behaviors;
*/
size_type max_element(const value_type* a, size_type n);

如果您能够在编译时验证实现始终保证满足子句中的后置条件，ensures前提是使用满足requires子句中前置条件的参数调用函数，则无需生成检查后置条件。

类似地，如果您验证所有调用者，当他们自己的先决条件得到满足时，max_element()只使用满足其先决条件的参数进行调用，那么在函数入口处检查是不必要的。

上面的例子来自ACSL by Example。这个库在ACSL中提供了许多函数契约。为合同提供了 C 中的实现。这些实现已经过静态形式化验证，以保证后置条件适用于所有带有满足前置条件的参数的调用。因此，后置条件不需要运行时检查。编译器可以将注释视为注释（它们是，使用/*@ ... */语法）。

Answer 3

契约式设计旨在确保正确实施——代码相对于调用者和被调用者之间的预期 API 正确编写。理想情况下，您可以在开发和 alpha 测试环境中使用静态分析工具和运行时检查来验证合约是否得到维护。希望到那时您已经发现了与 API 错误相关的任何实现错误。除非您试图追踪错误，否则您可能不会对 beta 和生产环境使用运行时检查。