6

如果我写这个：

public sealed class Foo
{
    private int count;
    private object owner;
    private void Bar()
    {
        Contract.Requires(count > 0);
        Contract.Ensures(owner == null || count > 0);

        if (count == 1)
            owner = null;
        --count;
    }
}

静态合约检查器可以证明所有断言。

但如果我改写这个：

public sealed class Foo
{
    private int count;
    private object owner;
    private void Bar()
    {
        Contract.Requires(count > 0);
        Contract.Ensures(owner == null || count > 0);

        --count;
        if (count == 0)
            owner = null;
    }
}

它声称后置条件owner == null || count > 0未经证实。

我想我可以证明第二种形式不违反这个后置条件：

// { count > 0 } it's required
--count;
// { count == 0 || count > 0 } if it was 1, it's now zero, otherwise it's still greater than zero
if (count == 0)
{
    // { count == 0 } the if condition is true
    owner = null;
    // { count == 0 && owner == null } assignment works
}
// { count == 0 && owner == null || count != 0 && count > 0 } either the if was entered or not
// { owner == null || count > 0 } we can assume a weaker postcondition

我的证明有问题吗？

我在证明中添加了断言作为Contract.Assert对代码的调用，我得出的结论是，如果我只添加这个断言，它就可以证明后置条件：

--count;
Contract.Assert(count == 0 || count > 0)
if (count == 0)
    owner = null;

但是，如果我现在将相同的断言更改为“更自然”的方式，它会失败：

--count;
Contract.Assert(count >= 0)
if (count == 0)
    owner = null;

预计这两个断言是等价的，但静态检查器对它们的处理方式不同。

（顺便说一下，我使用的是 VS10 的 beta 2）

4

2 回答 2

1

我不希望这个高度复杂的证明器处于完全工作状态，因为它毕竟只是一个测试版。我认为这是一个错误，或者至少是值得向开发人员提出的一点，因为这是自动进行静态检查的非常简单的事情。

无论如何，从外观上看，确保标记只是用来说明静态合同检查器是否能够确保条件。这并不意味着条件无效，它只是意味着它找不到证明。

我会更担心它说确保某些无效的情况。 那将被视为一个错误！

于 2009-12-17T17:34:11.347 回答
0

警告：我对 .net 合同系统的细节一无所知。

但是，我可以告诉你：实际上不可能（参见停止问题）为断言生成一个完整的证明者，就像这个系统所支持的那样丰富。

那么：这是一个错误吗？不。

另一方面，暗示这可能是证明者的实现者可能想要添加到他们的系统中的常见情况似乎是合理的。

于 2009-12-17T17:17:43.363 回答