mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
29 lines
573 B
Plaintext
29 lines
573 B
Plaintext
|
|
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).
|
|
*)
|