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
|
use int.Int
let f ()
ensures { result = 2 }
= let ref x = 0 in
let ref i = 0 in
while i < 2 do
variant { 2 - i }
invariant { x >= 0 }
x <- x + 1;
i <- i + 1
done;
x
(*
counterexample: `x = 0`, `i = 2` at beginning of the loop.
The execution of `f` with the counterexample:
- terminates normally if executed concretely;
- terminates in error if executed abstractly (postcondition fails)
It is a real counterexample due to underspecification (weak loop
invariant).
*)
|
