Counterexamples for labels bug
On the ref_mono.mlw example, the last case (Postcondition of test_loop
) does not include the value for the variables of "x at L" and "x at M". The invariant should appear in the task so these locations labels should appear too:
label M in
while !x > 0 do
(* x = 0 (0x0) *)
invariant { !x > !x at L + !x at M }
variant { !x }
x := !x - 1
done
should be:
label M in
while !x > 0 do
(* x = 0 (0x0) *)
invariant { !x > !x at L + !x at M }
(* x = ???, x at L = ???, x at M = ??? *)
variant { !x }
x := !x - 1
done