代码契约静态检查器是否应该能够检查算术界限？

Question

（也发布在 MSDN 论坛上 - 但据我所知，这并没有获得太多流量。）

我一直在尝试提供 Assert 和 Assume 的示例。 这是我得到的代码：（

public static int RollDice(Random rng)
{
    Contract.Ensures(Contract.Result<int>() >= 2 &&
                     Contract.Result<int>() <= 12);

    if (rng == null)
    {
        rng = new Random();
    }
    Contract.Assert(rng != null);

    int firstRoll = rng.Next(1, 7);
    Contract.Assume(firstRoll >= 1 && firstRoll <= 6);

    int secondRoll = rng.Next(1, 7);
    Contract.Assume(secondRoll >= 1 && secondRoll <= 6);

    return firstRoll + secondRoll;
}

当然，能够传递空引用而不是现有的随机引用纯粹是出于教学目的。）

我希望如果检查器知道这一点firstRoll 和 secondRoll 均在 [1, 6] 范围内，可以算出总和在 [1, 6] 范围内代码>[2, 12]。

这是一个不合理的希望吗？ 我意识到这是一件棘手的事情，要弄清楚可能会发生什么......但我希望检查器足够聪明:)

如果现在不支持这一点，这里有人知道它是否可能在不久的将来得到支持吗？未来如何？

编辑：我现在发现静态检查器中有非常复杂的算术选项。 使用“高级”文本框，我可以从 Visual Studio 中尝试它们，但据我所知，没有对它们的作用进行适当的解释。

Answer 1

我已经在MSDN论坛上找到了答案。 事实证明我已经快到了。 基本上，如果您拆分“and-ed”合同，静态检查器效果会更好。 因此，如果我们将代码更改为：

public static int RollDice(Random rng)
{
    Contract.Ensures(Contract.Result<int>() >= 2);
    Contract.Ensures(Contract.Result<int>() <= 12);

    if (rng == null)
    {
        rng = new Random();
    }
    Contract.Assert(rng != null);

    int firstRoll = rng.Next(1, 7);
    Contract.Assume(firstRoll >= 1);
    Contract.Assume(firstRoll <= 6);
    int secondRoll = rng.Next(1, 7);
    Contract.Assume(secondRoll >= 1);
    Contract.Assume(secondRoll <= 6);

    return firstRoll + secondRoll;
}

那就可以正常工作了。 这也意味着该示例更加有用，因为它强调了检查器确实可以更好地处理分离的合同。

Answer 2

我不知道 MS Contracts Checker 工具，但范围分析是一种标准的静态分析技术； 它广泛应用于商业静态分析工具中，用于验证下标表达式是否合法。

MS Research 在此类静态分析方面拥有良好的记录，因此我希望进行此类范围分析成为合同检查器的目标，即使目前尚未检查。