Is this a bug in the static contract controller?

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

Static contract verification can prove all the claims.

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

He claims that the postcondition owner == null || count > 0 owner == null || count > 0 not confirmed.

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

 // { count > 0 } it required --count; // { count == 0 || count > 0 } if it was 1, it now zero, otherwise it 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 there something wrong with my proof?

I added assertions in my proof as Contract.Assert calls the code, and I came to the conclusion that if I add only this one, he will be able to prove the postcondition:

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

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

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

These two statements were expected to be equivalent, but the static controller views them differently.

(By the way, I am using beta version 2 of VS10)

Answer 1

I would not expect this very complex thing to be in a fully operational state, since it is just a beta version. I think this is a mistake, or at least worth raising with the developers, because it is a very simple task for static checking automatically.

In any case, according to things, the collateral token just needs to say whether the static contract controller can provide the condition or not. This does not mean that the condition is invalid, it simply means that he cannot find evidence.

I would be much more concerned about cases where he says that something is guaranteed, that it is invalid. This will be considered a mistake!

Answer 2

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

However, I can tell you the following: it is literally impossible (for example, a problem with stopping) to create a full version for statements as rich as the one that this system apparently supports.

So: is this a mistake? Not.

On the other hand, it seems plausible to suggest that this may be a common case that program developers might want to add to their system.