.net - 这是静态合约检查器中的错误吗？

Question

如果我这样写:

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)

Answer 1

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

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

我会更担心它说某些内容是无效的。 这将被视为错误!