代码契约确保 for 循环未经验证

Question

我刚刚开始尝试 .Net 代码契约（在 VS2010 Ultimate .Net 4 中），试图了解静态检查器可以证明什么和不能证明什么。

我正在尝试以下示例：-

public int Mult(int num1, int num2)
    {
        Contract.Requires(num2 >= 0);
        Contract.Ensures(Contract.Result<int>() == (num1 * num2));
        int result = 0;
        for (int i = 0; i < num2; i++)
        {
            result = result + num1;
        }
        return result;
    }

即，通过重复相加来简单实现乘法函数。

静态检查器无法验证是否满足后置条件：-

CodeContracts: ensures unproven: Contract.Result<int>() == (num1 * num2)

我的函数实际上没有正确计算乘积..还是静态检查器无法验证 Requires 的其他原因？循环的存在是否会导致困难？

如果静态检查器在存在循环时很难验证事物，我可以想象一直有很多警告会变得非常烦人。

我不喜欢输入“假设”来告诉它我认为发生了什么，因为通常我的无效假设首先是导致错误的原因！

那么，当静态检查器无法证明某些事情时，我们如何才能帮助它呢？ 例如，我可以将该函数重写为递归函数 - 那么检查器是否能够更轻松地验证它？ （函数式编程的拥护者可能会说这就是它应该首先编写的方式 - 不改变状态等！）。我还可以通过哪些其他方式更改代码以使静态检查器更容易使用？

谢谢 ！：）

Answer 1

静态检查器永远无法证明这一点，但运行时检查器可以。

静态检查器在编译时应用。为了能够证明你的 Ensures，它必须能够充分分析你的算法和你正在做的事情。它没有那么强大。

当然，每次函数退出时，运行时检查器都会验证 Ensures，并且通过适当的单元测试，这应该证明 Ensures 的有效性。