这是静态合同检查器中的错误吗？

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

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

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

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