1

我收到以下包含代码合同的代码的警告。

public static int Min(IEnumerable<int> set)
{
    Contract.Requires(set != null);
    Contract.Requires(set.Any());

    Contract.Ensures(Contract.ForAll(set, x => x >= Contract.Result<int>()));

    int min = set.Min();

    return min;
}

static void Main(string[] args)
{
    Console.WriteLine(Min(new int[] {3,4,5}));
    Console.WriteLine(Min(new int[] {})); // should fail
}

我收到以下警告：

Requires unproven: set.Any() on Min(new int[] {3,4,5})

Ensures unproven: Contract.ForAll(set, x => x > Contract.Result<int>())

两个问题：

  1. 我的后置条件声明 x >= Contract.Result()，但“确保未经证实”的警告声明 x > Contract.Result()。（Greather or equal vs. Greather）这怎么会发生？

  2. 为什么不能在上面的语句中证明 set.Any() ？

先感谢您。

4

2 回答 2

1

该Ensures子句不适用于 allIEnumerable的开头。您可以编写一个IEnumerable在第一次枚举时返回一个序列（例如1, 2, 3），第二次返回另一个列表（例如0）。它是一个具有任意实现的接口。

IEnumerable的通常有很多（可能生成的）东西在幕后进行。我不认为 CC 可以看穿这一点，即使具体的运行时类型以某种方式已知。

CC 甚至能够启发式地推理IEnumerable's 吗？那对我来说是新的。它必须假设如果多次枚举序列不会改变（在数据库查询的情况下这是微不足道的错误）。

让我作为主观的旁注指出，我发现 CC 检查器太有限而无法使用。证明有趣的属性会带来很多麻烦。它不能很好地处理抽象。

于 2012-12-12T12:22:29.313 回答
0

STATIC 代码检查器无法确定该集合包含任何数据。如果您考虑一下，检查器不知道各种方法和属性的作用，除非在方法本身内部定义了一些协定。

在您的情况下，检查器不知道扩展方法 Any() 或 Min() 的结果可能是什么，因此它无法验证任何 Requires 和 Ensures。

您可以通过更改参数的类型获得更少的警告，但最终代码检查器仍然无法确保您的代码能够满足 Min(...) 的要求。

如果将类型更改为 int[] 或 List，某些警告可能会消失。以下代码不返回任何警告：

    public static int Min(List<int> set)
    {
        Contract.Requires(set != null);
        Contract.Requires(set.Count>0);


        Contract.Ensures(Contract.ForAll(set, x => x >= Contract.Result<int>()));

        int min = set.Min();

        return min;
    }

    static void Main(string[] args)
    {

        Console.WriteLine(Min(new List<int> { })); // should fail
        Console.WriteLine(Min(new List<int> { 3, 4, 5 }));
        Console.ReadKey();
    }

当然，如果您运行此代码，它将失败并出现异常，因此代码检查器可能足够聪明，可以检测到这一点。

如果您保留原始订单，您仍然会收到警告：

        Console.WriteLine(Min(new List<int> { 3, 4, 5 }));
        Console.WriteLine(Min(new List<int> { })); // should fail

在这两种情况下，您还会得到一些疯狂的建议，例如在 Main() 中添加 Contract.Ensures(false)。

于 2012-12-12T12:47:47.597 回答