Spec#是一个流行的微软研究项目,它允许一些 DBC 构造,例如检查后置条件和前置条件。例如,可以使用前置条件和后置条件以及循环不变量来实现二进制搜索。这个例子和更多:
public static int BinarySearch(int[]! a, int key)
requires forall{int i in (0: a.Length), int j in (i: a.Length); a[i] <= a[j]};
ensures 0 <= result ==> a[result] == key;
ensures result < 0 ==> forall{int i in (0: a.Length); a[i] != key};
{
int low = 0;
int high = a.Length - 1;
while (low <= high)
invariant high+1 <= a.Length;
invariant forall{int i in (0: low); a[i] != key};
invariant forall{int i in (high+1: a.Length); a[i] != key};
{
int mid = (low + high) / 2;
int midVal = a[mid];
if (midVal < key) {
low = mid + 1;
} else if (key < midVal) {
high = mid - 1;
} else {
return mid; // key found
}
}
return -(low + 1); // key not found.
}
请注意,使用 Spec# 语言会产生对 DBC 结构的编译时检查,这对我来说是利用 DBC 的最佳方式。通常,依赖运行时断言成为生产中的一个令人头疼的问题,人们通常选择使用异常来代替。
还有其他语言将 DBC 概念作为一流的结构,即Eiffel,它也可用于 .NET 平台。