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

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 ||计数> 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

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

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

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

Answer 2

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

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

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

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