如果该代码契约静态检查能够检查算术约束？

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;
}

（关于能够在一个空引用，而不是现有的Random引用传递该业务是纯粹的教学，当然。）

我曾希望，如果检查知道firstRoll和secondRoll各自范围[1, 6]，它能够制定出了金额为范围[2, 12]。

这是一个不合理的希望吗？我意识到这是一个棘手的业务，制定出可能会发生什么......但我希望的检查将足够聪明：）

如果这不是现在支持，并在这里认识的人，如果它有可能在不久的十岁上下的将来得到支持？

编辑：现在我已经发现有在静态检测算法非常复杂的选项。使用“高级”文本框中，我可以尝试他们从Visual Studio，但有他们做什么，只要我可以告诉没有像样的解释。

Answer 1

我已经在MSDN论坛的答案。原来我是非常接近那里。基本上，如果你打出了“和主编”合同中的静态检测效果更好。所以，如果我们的代码改成这样：

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的合同检查工具，但范围分析是标准的静态分析技术;它被广泛应用于商业的静态分析工具来验证下标表达式是合法的。

MS研究已经在这种静态分析的良好记录，所以我希望做这样的范围分析，以合同检查的目标，即使目前不检查。