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
29
30
31
32
33
34
35
36
37
38
39
|
module LoopInvariant
use int.Int
(* use array.Array *)
(* let h () = *)
(* let a = Array.make 10 0 in *)
(* for i = 0 to 9 do *)
(* invariant { forall j. 0 <= j < i -> a[j] = 1 } *)
(* a[i] <- a[i] + 1 *)
(* done *)
let f () =
let ref x1 = 0 in
let ref x2 = 0 in
for i = 0 to 1 do
invariant { i > 0 -> x1 = 1 }
if i = 0 then
x1 <- x1 + 1
else
x2 <- x2 + 1
done
end
module PostCondition
use int.Int
val ref z: int
let g ()
writes { z }
ensures { z > old z }
= z <- z + 1
let f () =
z <- 0;
g ();
assert { z = 1 }
end
|
