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)