1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
use int.Int
let f (z: int) =
let ref x1 = z in
let ref x2 = 0 in
let ref i = 0 in
while i < 2 do
variant { 2 - i }
invariant { i > 0 -> x1 >= 0 }
if i = 0 then
x1 <- x1 + 1
else
x2 <- x2 + 1;
i <- i + 1
done
(*
counterexample: `x1 = -2`, `i = 0` at the beginning of the loop.
The execution of `f` with the counterexample:
- terminates normally if executed concretely;
- terminates in error if executed abstractly (invariant preservation
fails)
It is a real counterexample due to underspecification (weak loop
invariant).
*)
|
