2

我有这个代码：

using System;
using System.Diagnostics.Contracts;

namespace TestCodeContracts
{
    class Program
    {
        public static int Divide(int numerator, int denominator, out int remainder)
        {
            Contract.Requires<ArgumentException>(denominator != 0);
            Contract.Requires<ArgumentException>(numerator != int.MinValue || denominator != -1, "Overflow");
            Contract.Ensures(Contract.Result<int>() == numerator / denominator);
            Contract.Ensures(Contract.ValueAtReturn<int>(out remainder) == numerator % denominator);

            remainder = numerator % denominator;
            return numerator / denominator;
        }

        static void Main(string[] args)
        {
            int remainder;
            Console.WriteLine(Divide(10, 6, out remainder));
            Console.WriteLine(Divide(5, remainder, out remainder));

            Console.WriteLine(Divide(3, 0, out remainder));

            Console.Read();
        }
    }
}

在第一次 Divide 调用中，如果我替换6为0，则静态分析会正确警告它。

如果我替换6为5，那么我（正确地）在第二次 Divide 调用时收到警告。

但是，无论如何，我在第三次 Divide 电话中从未收到任何警告。相反，我只是得到一个运行时错误。

为什么静态分析器无法检测到第三行是否违反合同？

我在 Windows 8 64 位上使用 Visual Studio 2012。代码合同是Microsoft Code Contracts (devlabs_TS) 1.4.51019.0 for .NET（这似乎是截至 2012 年 12 月的最新版本）。

4

2 回答 2

3

我在代码合同论坛上发布了这个。已确认这确实是一个错误，并将对其进行修复。

错误是静态验证器认为 Divide(3, 0... ) 无法访问

(...)

我们将修复错误。

于 2012-12-13T11:48:56.593 回答
1

这是一个有趣的问题。

我最终简化Divide为：

public static int Divide(int numerator, int denominator)
{
    Contract.Requires<ArgumentException>(denominator != 0);
    return numerator / denominator;
}

这会引发正确的警告：

static void Main(string[] args)
{
    Console.WriteLine(Divide(10, 10));
    Console.WriteLine(Divide(10, 0));
}

请注意，我发现您通常必须重建而不是构建，即使只有一个项目。必须有在重建时清理的代码合同人工制品。

这不会引发警告：

static void Main(string[] args)
{
    Console.WriteLine(Divide(10, 9));
    Console.WriteLine(Divide(10, 0));
}

我可以触发警告的唯一方法是第一个除法的分母是否为 10（显然它在为 0 时也有效）。

这似乎是一个错误——我会向代码合同团队发送一封电子邮件，看看他们怎么说。

于 2012-12-10T02:00:45.767 回答