Merge branch '863-forward-propagation-strategy-accept-optionnal-arguments' into ...
[why3.git] / examples / vacid_0_sparse_array.mlw
blob96ea0de7a617637b7b30eb259176b068e455a682
1 module SparseArray
3 (*
4       If the sparse array contains three elements x y z, at index
5       a b c respectively, then the three arrays look like this:
7               b     a      c
8 values +-----+-+---+-+----+-+----+
9        |     |y|   |x|    |z|    |
10        +-----+-+---+-+----+-+----+
12 index  +-----+-+---+-+----+-+----+
13        |     |1|   |0|    |2|    |
14        +-----+-+---+-+----+-+----+
16         0 1 2  n=3
17 back   +-+-+-+-------------------+
18        |a|b|c|                   |
19        +-+-+-+-------------------+
23   use int.Int
24   use array.Array
26   constant maxlen : int = 1000
28   type sparse_array 'a = { values : array 'a;
29                            index  : array int;
30                            back   : array int;
31                    mutable card   : int;
32                            def    : 'a; }
33   invariant {
34     0 <= card <= length values <= maxlen /\
35     length values = length index = length back /\
36     forall i : int.
37       0 <= i < card ->
38       0 <= back[i] < length values /\ index[back[i]] = i
39   } by {
40     values = make 0 (any 'a);
41     index  = make 0 0;
42     back   = make 0 0;
43     card   = 0;
44     def    = any 'a
45   }
47   predicate is_elt (a: sparse_array 'a) (i: int) =
48     0 <= a.index[i] < a.card /\ a.back[a.index[i]] = i
50   function value (a: sparse_array 'a) (i: int) : 'a =
51     if is_elt a i then
52       a.values[i]
53     else
54       a.def
56   function length (a: sparse_array 'a) : int = Array.length a.values
58   (* creation *)
60   val malloc (n:int) : array 'a ensures { Array.length result = n }
62   let create (sz: int) (d: 'a)
63     requires { 0 <= sz <= maxlen }
64     ensures { result.card = 0 /\ result.def = d /\ length result = sz }
65   = { values = malloc sz;
66       index  = malloc sz;
67       back   = malloc sz;
68       card   = 0;
69       def    = d }
71   (* access *)
73   let test (a: sparse_array 'a) i
74     requires { 0 <= i < length a }
75     ensures { result=True <-> is_elt a i }
76   = 0 <= a.index[i] < a.card && a.back[a.index[i]] = i
78   let get (a: sparse_array 'a) i
79     requires { 0 <= i < length a }
80     ensures { result = value a i }
81   = if test a i then
82       a.values[i]
83     else
84       a.def
86   (* assignment *)
88   use map.MapInjection as MI
90   lemma permutation :
91     forall a: sparse_array 'a.
92     (* sparse_array invariant *)
93       Array.(0 <= a.card <= Array.length a.values <= maxlen /\
94       length a.values = length a.index = length a.back /\
95       forall i : int.
96         0 <= i < a.card ->
97         0 <= a.back[i] < length a.values /\ a.index[a.back[i]] = i) ->
98     (* sparse_array invariant *)
99     a.card = a.length ->
100     forall i: int. 0 <= i < a.length -> is_elt a i
101       by MI.surjective a.back.elts a.card
102       so exists j. 0 <= j < a.card /\ a.back[j] = i
105   let set (a: sparse_array 'a) i v
106     requires { 0 <= i < length a }
107     ensures { value a i = v /\
108       forall j:int. j <> i -> value a j = value (old a) j }
109   = a.values[i] <- v;
110     if not (test a i) then begin
111       assert { a.card < length a };
112       a.index[i] <- a.card;
113       a.back[a.card] <- i;
114       a.card <- a.card + 1
115     end
119 module Harness
121   use SparseArray
123   type elt
124   val constant default : elt
126   val constant c1 : elt
127   val constant c2 : elt
129   let harness () =
130     let a = create 10 default in
131     let b = create 20 default in
132     let get_a_5 = get a 5 in assert { get_a_5 = default };
133     let get_b_7 = get b 7 in assert { get_b_7 = default };
134     set a 5 c1;
135     set b 7 c2;
136     let get_a_5 = get a 5 in assert { get_a_5 = c1 };
137     let get_b_7 = get b 7 in assert { get_b_7 = c2 };
138     let get_a_7 = get a 7 in assert { get_a_7 = default };
139     let get_b_5 = get b 5 in assert { get_b_5 = default };
140     let get_a_0 = get a 0 in assert { get_a_0 = default };
141     let get_b_0 = get b 0 in assert { get_b_0 = default };
142     ()
144   val predicate (!=) (x y : elt)
145     ensures { result <-> x <> y }
147   exception BenchFailure
149   let bench () raises { BenchFailure -> true } =
150     let a = create 10 default in
151     let b = create 20 default in
152     if get a 5 != default then raise BenchFailure;
153     if get b 7 != default then raise BenchFailure;
154     set a 5 c1;
155     set b 7 c2;
156     if get a 5 != c1 then raise BenchFailure;
157     if get b 7 != c2 then raise BenchFailure;
158     if get a 7 != default then raise BenchFailure;
159     if get b 5 != default then raise BenchFailure;
160     if get a 0 != default then raise BenchFailure;
161     if get b 0 != default then raise BenchFailure