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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
|
(** Setting all the elements of an array to zero *)
module SetZeros
use int.Int
use array.Array
let set_zeros (a : array int) =
ensures { forall j: int. 0 <= j < a.length -> a[j] = 0 }
for i = 0 to a.length - 1 do
invariant { forall j: int. 0 <= j < i -> a[j] = 0 }
a[i] <- 0
done
let harness () =
let a0 = make 42 1 in
set_zeros a0;
assert { length a0 = 42 };
assert { a0[12] = 0 }
end
(** Checking that an array contains only zeros *)
module AllZeros
use int.Int
use array.Array
use ref.Refint
predicate all_zeros (a: array int) (hi: int) =
forall i: int. 0 <= i < hi -> a[i] = 0
(** with a for loop (a bit naive, since it always scans the whole array) *)
let all_zeros1 (a: array int) : bool
ensures { result <-> all_zeros a a.length }
=
let res = ref True in
for i = 0 to length a - 1 do
invariant { !res <-> all_zeros a i }
if a[i] <> 0 then res := False
done;
!res
(** with a while loop, stopping as early as possible *)
let all_zeros2 (a: array int) : bool
ensures { result <-> all_zeros a a.length }
=
let res = ref True in
let i = ref 0 in
while !res && !i < length a do
invariant { 0 <= !i <= a.length }
invariant { !res <-> all_zeros a !i }
variant { a.length - !i }
res := (a[!i] = 0);
incr i
done;
!res
(** no need for a Boolean variable, actually *)
let all_zeros3 (a: array int) : bool
ensures { result <-> all_zeros a a.length }
=
let i = ref 0 in
while !i < length a && a[!i] = 0 do
invariant { 0 <= !i <= a.length }
invariant { all_zeros a !i }
variant { a.length - !i }
incr i
done;
!i = length a
(** with a recursive function *)
let all_zeros4 (a: array int) : bool
ensures { result <-> all_zeros a a.length }
=
let rec check_from (i: int) : bool
requires { 0 <= i <= a.length }
requires { all_zeros a i }
variant { a.length - i }
ensures { result <-> all_zeros a a.length }
= i = length a || a[i] = 0 && check_from (i+1)
in
check_from 0
(** divide-and-conqueer *)
predicate zero_interval (a: array int) (lo hi: int) =
forall i: int. lo <= i < hi -> a[i] = 0
use int.ComputerDivision
let all_zeros5 (a: array int) : bool
ensures { result <-> all_zeros a a.length }
=
let rec check_between (lo hi: int) : bool
requires { 0 <= lo <= hi <= a.length }
variant { hi - lo }
ensures { result <-> zero_interval a lo hi }
=
hi <= lo ||
let mid = lo + div (hi - lo) 2 in
a[mid] = 0 && check_between lo mid && check_between (mid+1) hi
in
check_between 0 (Array.length a)
end
|
