Is this a bug in the static contract checker?

Question

If I write this:

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;
    }
}

The static contract checker can prove all assertions.

But if I write this instead:

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;
    }
}

It claims the postcondition owner == null || count > 0 is unproven.

I think I can prove the second form does not violate this postcondition:

// { 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

Is something wrong with my proof?

I added the assertions in my proof as Contract.Assert calls to the code, and I came to the conclusion that if I add just this one, it manages to prove the postcondition:

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

But, if I now change that same assertion to a "more natural" way, it fails:

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

It would be expected that those two assertions were equivalent, but the static checker treats them differently.

(I'm using beta 2 of VS10 by the way)

Answer 1

I wouldn't expect this highly complex prover thing to be in a fully working state yet since it's just a beta after all. I think it is a bug or at least a point worth raising with the developers, because this is a very simple thing to static check automatically.

Anyway, by the looks of things, the ensures marker is just there to say whether the static contract checker is able to ensure the condition or not. This does not imply that the condition is not valid, it just means it can't find a proof.

I would be much more worried about cases where it says something is ensured which is invalid. That would count as a bug!

Answer 2

Caveat: I know absolutely nothing about the specifics of the .net contract system.

However, I can tell you this: it's literally not possible (cf. halting problem) to produce a complete prover for assertions as rich as the one that it appears this system supports.

So: is this a bug? No.

On the other hand, it seems plausible to suggest that this might be a common case that the implementors of the prover might want to add to their system.