4

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

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

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

这些条件以简洁明了的方式清楚地指定了 Factorial 的行为。我的问题是，它们是否可以通过代码合同来表达。

前提是微不足道的：

Contract.Requires(n >= 0)

条件后置条件可以用

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

但我不喜欢这里需要“if”语句的方式，因为它使前置条件和后置条件的简单列表更难阅读。我希望我们会有类似的东西

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

最后但并非最不重要的一点是，我不知道如何表达这一点，这是关于数学的常见符号：

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

我猜我需要某种循环，但这会复制整个实现。有什么聪明的方法来表达这样的符号吗？

先感谢您。

4

2 回答 2

4

您正在寻找的是单元测试，而不是代码合同。

通常，检查类似于if n=0, then f(n) = 1并且if n=3, then 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 并没有完全指定算法。

我不认为 Code Contract 的工作是详细指定算法。算法由方法指定。

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

没想到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);
于 2012-11-20T08:50:17.137 回答
1

您可以尝试以下操作：

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仅在调试配置上构建来解决。

于 2012-11-20T11:37:16.170 回答