代码之家 › 专栏 › 技术社区 › Jon Skeet

代码协定静态检查器是否能够检查算术绑定?

code-contracts math static-analysis

33

Jon Skeet · 技术社区 · 15 年前

(也) posted on the MSDN forum -但据我所见,交通不太拥挤。)

我一直试图提供一个 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中试用它们,但据我所知,它们所做的工作没有像样的解释。

2 回复 | 直到 9 年前

1

14

Jon Skeet 15 年前

我在msdn论坛上得到了答案。结果我就快到了。基本上,如果拆分“和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;
}

那没问题。它还意味着该示例更有用,因为它突出了检查程序做通过分离的合同更好地工作。

2

1

Ira Baxter 15 年前

我不知道MS合同检查器工具,但范围分析是一种标准的静态分析技术;它广泛用于商业静态分析工具中,以验证下标表达式是否合法。

MS Research在这种静态分析方面有很好的跟踪记录,所以我希望做这种范围分析是合同审查员的目标,即使目前没有检查。