35

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

我一直在尝试提供Assertand的示例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 中试用它们，但据我所知，它们的作用没有像样的解释。

4

2 回答 2

14

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

这没有任何问题。这也意味着该示例更加有用，因为它突出了检查器在分离合同时确实可以更好地工作这一点。

于 2009-08-07T20:27:26.673 回答
1

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

MS Research 在这种静态分析方面有着良好的记录，所以我希望进行这种范围分析成为合同检查器的目标，即使目前没有检查。

于 2009-08-07T14:10:46.743 回答