janhaag/PSE2011 — Issue #20: Multiple specification statements not supported
Author: danielbruns
Created: 2012-02-24 12:49:12+00:00
State: open

Hi, in the following program the 3 invariants are rejected. This is allowed according to the language specificatiuon in the design document. And is necessary because of issue #12.
main (int[] a, int x)
assume length(a) > 0;
{
int i = 1;
x = a[0];
while (i < length(a))
invariant forall j (0,i-1) (x >= a[j]);
invariant (0 < i) & (i <= length(a));
invariant exists j (0,i-1) x == a[j];
{
if (x < a[i]) { x = a[i]; }
i = i +1;
}
}
ensure forall i (0,length(a)-1) x >= a[i];
ensure exists i (0,length(a)-1) x == a[i];