设计契约或代码契约的看法

Question

我目前正在阅读有关设计合同/代码合同的更多信息。据我所知，它是编写合同（不变量、前置条件和后置条件），以确保代码可以有序维护。它还通过基于检查和平衡的良好定义机制来保证预防错误。

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

我非常感谢人们与我分享有关设计合同的观点和经验。缺点或优点都受欢迎。

- user1004413

Answer 1

通常这样的框架支持运行时检查和静态分析。后者在编译时（或之前）执行，不会减慢代码速度。前者可能会影响性能。 Microsoft Research Code Contracts 项目是一个很好的例子。您可以配置系统，使其满足以下条件：

- 静态分析在编译时应用一部分可能的合同实施，甚至在设计环境中也可以实现； - 运行时检查对于在调试模式下编译的所有代码都是启用的；以及 - 对于在发布模式下编译的公共API，启用了一部分运行时检查（非公共代码没有运行时检查）。

这通常是性能和健壮性之间的一个很好的折衷方案。

- Olly

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);

如果你能够在编译时验证实现始终保证在使用满足requires条款的参数调用函数时，ensures子句中的后置条件得到满足，则无需为后置条件生成检查。同样地，如果你验证所有调用方在满足自己的前置条件时仅使用满足其前置条件的参数调用max_element()，则不需要在函数入口处进行检查。以上示例来自ACSL by Example。该库提供了ACSL中的许多函数契约。这些合同的C实现已经被静态正式验证，以确保对于满足前置条件的所有调用，后置条件都成立。因此，后置条件不需要运行时检查。编译器可以将注释视为注释（它们使用/*@ ... */语法）。

- Pascal Cuoq

Answer 3

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

- Bert F