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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
|
module SparseArray
(*
If the sparse array contains three elements x y z, at index
a b c respectively, then the three arrays look like this:
b a c
values +-----+-+---+-+----+-+----+
| |y| |x| |z| |
+-----+-+---+-+----+-+----+
index +-----+-+---+-+----+-+----+
| |1| |0| |2| |
+-----+-+---+-+----+-+----+
0 1 2 n=3
back +-+-+-+-------------------+
|a|b|c| |
+-+-+-+-------------------+
*)
use int.Int
use array.Array
constant maxlen : int = 1000
type sparse_array 'a = { values : array 'a;
index : array int;
back : array int;
mutable card : int;
def : 'a; }
invariant {
0 <= card <= length values <= maxlen /\
length values = length index = length back /\
forall i : int.
0 <= i < card ->
0 <= back[i] < length values /\ index[back[i]] = i
} by {
values = make 0 (any 'a);
index = make 0 0;
back = make 0 0;
card = 0;
def = any 'a
}
predicate is_elt (a: sparse_array 'a) (i: int) =
0 <= a.index[i] < a.card /\ a.back[a.index[i]] = i
function value (a: sparse_array 'a) (i: int) : 'a =
if is_elt a i then
a.values[i]
else
a.def
function length (a: sparse_array 'a) : int = Array.length a.values
(* creation *)
val malloc (n:int) : array 'a ensures { Array.length result = n }
let create (sz: int) (d: 'a)
requires { 0 <= sz <= maxlen }
ensures { result.card = 0 /\ result.def = d /\ length result = sz }
= { values = malloc sz;
index = malloc sz;
back = malloc sz;
card = 0;
def = d }
(* access *)
let test (a: sparse_array 'a) i
requires { 0 <= i < length a }
ensures { result=True <-> is_elt a i }
= 0 <= a.index[i] < a.card && a.back[a.index[i]] = i
let get (a: sparse_array 'a) i
requires { 0 <= i < length a }
ensures { result = value a i }
= if test a i then
a.values[i]
else
a.def
(* assignment *)
use map.MapInjection as MI
lemma permutation :
forall a: sparse_array 'a.
(* sparse_array invariant *)
Array.(0 <= a.card <= Array.length a.values <= maxlen /\
length a.values = length a.index = length a.back /\
forall i : int.
0 <= i < a.card ->
0 <= a.back[i] < length a.values /\ a.index[a.back[i]] = i) ->
(* sparse_array invariant *)
a.card = a.length ->
forall i: int. 0 <= i < a.length -> is_elt a i
by MI.surjective a.back.elts a.card
so exists j. 0 <= j < a.card /\ a.back[j] = i
let set (a: sparse_array 'a) i v
requires { 0 <= i < length a }
ensures { value a i = v /\
forall j:int. j <> i -> value a j = value (old a) j }
= a.values[i] <- v;
if not (test a i) then begin
assert { a.card < length a };
a.index[i] <- a.card;
a.back[a.card] <- i;
a.card <- a.card + 1
end
end
module Harness
use SparseArray
type elt
val constant default : elt
val constant c1 : elt
val constant c2 : elt
let harness () =
let a = create 10 default in
let b = create 20 default in
let get_a_5 = get a 5 in assert { get_a_5 = default };
let get_b_7 = get b 7 in assert { get_b_7 = default };
set a 5 c1;
set b 7 c2;
let get_a_5 = get a 5 in assert { get_a_5 = c1 };
let get_b_7 = get b 7 in assert { get_b_7 = c2 };
let get_a_7 = get a 7 in assert { get_a_7 = default };
let get_b_5 = get b 5 in assert { get_b_5 = default };
let get_a_0 = get a 0 in assert { get_a_0 = default };
let get_b_0 = get b 0 in assert { get_b_0 = default };
()
val predicate (!=) (x y : elt)
ensures { result <-> x <> y }
exception BenchFailure
let bench () raises { BenchFailure -> true } =
let a = create 10 default in
let b = create 20 default in
if get a 5 != default then raise BenchFailure;
if get b 7 != default then raise BenchFailure;
set a 5 c1;
set b 7 c2;
if get a 5 != c1 then raise BenchFailure;
if get b 7 != c2 then raise BenchFailure;
if get a 7 != default then raise BenchFailure;
if get b 5 != default then raise BenchFailure;
if get a 0 != default then raise BenchFailure;
if get b 0 != default then raise BenchFailure
end
|
