代码合约：如何表达这些条件？

Question

我目前正在研究代码合同，并不完全确定Contract类的静态方法是否足以与条件的数学符号竞争。

假设我们有一个简单的阶乘方法：

int Factorial(int n);

我将表达以下条件：

Precondition:
n >= 0

Postconditions:
Factorial(n) = 1, in case n = 0
Factorial(n) = n*(n-1)*...*1, in case n > 0

这些条件清晰地规定了阶乘的行为方式。我的问题是，它们是否可以通过代码合同来表达。

前置条件很简单：

Contract.Requires(n >= 0)

条件后置条件可以使用以下方式表示：

if(n==0)
    Contract.Ensures(Contract.Result<int>() == 1);
if(n > 0)
    ...

但我不喜欢在这里使用“if”语句，因为它使得前置和后置条件的普通列表变得更难以阅读。我希望我们有类似以下的内容：

Contract.Ensures(...).InCase(...);

最后但同样重要的是，我不知道该如何表达这个关于数学的普遍符号:

n*(n-1)*...*1

我想我需要一些循环的方式，但这样会复制整个实现。有没有聪明的方法来表达这样的符号?

提前感谢你。

- mbue

Answer 1

您需要的是单元测试，而不是代码合同。

通常像“如果n = 0，则f（n）= 1”和“如果n = 3，则f（n）= 6”这样的检查是应该表达为单元测试的测试用例。

在您的情况下，我认为一个合适的后置条件应该是类似于“结果始终> = 1”的内容。没有更多的要求。

假设您的阶乘类看起来像这样：

public class Factorial
{
    public int Compute(int n)
    {
        if (n == 0)
            return 1;

        return n * Compute(n - 1);
    }
}

使用NUnit框架编写的适当的单元测试应该是：

[TestFixture]
public class FactorialTests
{
    [TestCase(0, 1)]
    [TestCase(1, 1)]
    [TestCase(2, 2)]
    [TestCase(7, 5040)]
    [TestCase(10, 3628800)]
    public void Compute_ReturnsCorrectResult(int n, int expectedResult)
    {
        var sut = new Factorial();

        Assert.AreEqual(expectedResult, sut.Compute(n));
    }
}

更新（评论后）

声明结果>=1并不能完全指定算法。

我认为代码契约的工作不是详细说明算法，而是由方法来指定算法。

如果代码契约像方法本身一样复杂，那么我们可能需要一个代码契约合同来验证代码契约是否执行正确的检查。这显然会导致无限递归。

我没想到编译器能够接受n*(n-1)*...*1。但某些类似于LINQ的通用范围运算符肯定是一个很好的补充，例如From(n).To(1).Product()或From(n).To(m).Sum()

如果有这样一种表示阶乘的形式（可能确实有），您肯定可以在代码中使用它，而不是使用代码契约。

更新2

只是为了好玩，我找到了一种使用LINQ计算阶乘的方式：

Enumerable.Range(1, n == 0 ? 1 : n).Aggregate((a, i) => a * i);

- Cristian Lupascu

---

不要认为这是真的。通过逻辑条件指定输出是非常普遍的，例如在使用 Hoare 规则时。声明 result >= 1 并不能完全指定算法。 - mbue

也许可以像代码合同支持量词（例如forall）一样，但您不在实现中使用它们。我没有预料到编译器会接受n （n-1） ... * 1。但是，以LINQ风格的某些通用范围运算符肯定是一个很好的补充，例如From(n).To(1).Product()或From(n).To(m).Sum()。 - mbue

@mbue 请查看我的回答更新。你提出了一些重要的观点，我认为最好将它们和回复作为回答的一部分。 - Cristian Lupascu

@mbue 对称性也可以是这样一个例子，而非负性则非常接近我上面提出的（“结果始终>= 1”）。 - Cristian Lupascu

@mbue 然而，将极其复杂的条件添加到代码中可能会降低可读性。 - Cristian Lupascu

Answer 2

您可以尝试以下方法：

Contract.Ensures(Contract.Result<int>() == AlternativeFactorial(n));

其中AlternativeFactorial是：

[Pure]
public static int AlternativeFactorial(int n)
{
    if(n==0)
        return 1;
    if(n > 0)
    {
        //Alternative implementation.
    }
}

当然，合同中使用的任何内容都应该是无副作用（纯净）的。

至于阶乘实现，我想不出比w0lf更紧凑的“替代”实现了。但你应该考虑将方法的返回值从int改为BigInteger。阶乘可以非常快地变得非常大。此外，请注意，在阶乘值上添加后置条件将几乎使您的方法返回结果所需的时间加倍。这可以通过仅在调试配置上构建CodeContracts来解决。

- Panos Rontogiannis

---

@w0lf 你说得对，我错过了问题的最后一部分。我会更新我的答案。 - Panos Rontogiannis

@w0lf 但这不是重复。您需要将算法实现的结果与被接受为正确的另一个算法的结果进行测试。重要的是有解决相同问题的不同实现（或算法）。否则那就没有意义了。您提出的使用单元测试的解决方案并不能替代使用CodeContracts。CodeContracts和单元测试应该一起使用。它们互补。 - Panos Rontogiannis

如果您有一个被认为是正确的实现，为什么不直接使用它呢？ - Cristian Lupascu

“重要的是拥有解决同一问题的不同实现（或算法）。” - 我很确定如果我对我的老板说了这句话，我会在下一秒钟被解雇。 - Cristian Lupascu

@w0lf 在没有上下文的情况下，我的话听起来有点过了。OP 正在尝试找出 CodeContracts 是否能“与条件的数学符号竞争”。你的老板会对此有何看法 ;) 关于你的另一个问题，有时人们会尝试解决已经有人解决过的问题。他们可能需要更快的解决方案或者一个节省内存的解决方案，或者他们只是想自己动手做。 - Panos Rontogiannis