janhaag/PSE2011 — Issue #6: Verification has false-positives and false-negatives
Author: danielbruns
Created: 2012-02-07 09:06:21+00:00
State: open

There are several proof obligations generated, but it is unclear which ones a program must fulfill in order to be deemed correct. Take the following program for instance:
main(){ int x; int y; while (y == 0){ x = x+1; } } ensure x >0;
It obviously fulfills its postcondition. Yet this should not be provable without an invariant.
However, the proof obligation "InvariantAndNotConditionToEnsure" says "true" (false-negative).
There is another proof obligation "WhileEnsureToRemaining" that reports "false" even in case there is an invariant given (false-positive).