如果Code Contracts静态检查器能够检查算术绑定吗？

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

这没有任何问题.这也意味着该示例更有用,因为它突出了检查器在分离出的合同中更好地工作的重点.