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
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
|
(* 'Checking a large routine' Alan Mathison Turing, 1949
One of the earliest proof of program.
The routine computes n! using only additions, with two nested loops.
*)
module CheckingALargeRoutine
use int.Int
use int.Fact
use ref.Ref
(* using 'while' loops, to keep close to Turing's flowchart *)
let routine (n: int) requires { n >= 0 } ensures { result = fact n } =
let r = ref 0 in
let u = ref 1 in
while !r < n do
invariant { 0 <= !r <= n /\ !u = fact !r }
variant { n - !r }
let s = ref 1 in
let v = !u in
while !s <= !r do
invariant { 1 <= !s <= !r + 1 /\ !u = !s * fact !r }
variant { !r - !s }
u := !u + v;
s := !s + 1
done;
r := !r + 1
done;
!u
(* using 'for' loops, for clearer code and annotations *)
let routine2 (n: int) requires { n >= 0 } ensures { result = fact n } =
let u = ref 1 in
for r = 0 to n-1 do invariant { !u = fact r }
let v = !u in
for s = 1 to r do invariant { !u = s * fact r }
u := !u + v
done
done;
!u
let downward (n: int) requires { n >= 0 } ensures { result = fact n } =
let r = ref n in
let u = ref 1 in
while !r <> 0 do
invariant { 0 <= !r <= n /\ !u * fact !r = fact n }
variant { !r }
let s = ref 1 in
let v = !u in
while !s <> !r do
invariant { 1 <= !s <= !r /\ !u = !s * v }
variant { !r - !s }
u := !u + v;
s := !s + 1
done;
r := !r - 1
done;
!u
end
|
