vacid_0_sparse_array.mlw 4.5 KB
Newer Older
1

2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
(*
      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 
val   +-----+-+---+-+----+-+----+
      |     |y|   |x|    |z|    |
      +-----+-+---+-+----+-+----+

idx   +-----+-+---+-+----+-+----+
      |     |1|   |0|    |2|    |  
      +-----+-+---+-+----+-+----+

       0 1 2  n=3
back  +-+-+-+-------------------+
      |a|b|c|                   |
      +-+-+-+-------------------+

*)

22
23
24
25
26
27
28
29
30
31
{
  use array.ArrayLength as A

  logic maxlen : int = 1000

  type elt
  logic default : elt
  logic c1 : elt
  logic c2 : elt

32
  type array 'a = A.t 'a
33

34
  logic (#) (a : array 'a) (i : int) : 'a = A.select a i
35

36
37
38
39
40
  type sparse_array = SA (sa_val  : array elt) 
                         (sa_idx  : array int)
                         (sa_back : array int)
                         (sa_sz   : int)
                         (sa_n    : int)
41

42
  logic is_elt (a : sparse_array) (i : int) =
43
    let (SA val idx back _ n) = a in
44
45
    0 <= idx#i < n and back#(idx#i) = i

46
  logic model (a : sparse_array) (i : int) : elt =
47
48
    if is_elt a i then
      (sa_val a)#i
49
50
51
    else
      default

52
  logic invariant (a : sparse_array) = 
53
    let (SA val idx back sz n) = a in
54
    0 <= n <= sz <= maxlen and
55
    forall i : int. 0 <= i < n -> 0 <= back#i < sz and idx#(back#i) = i
56

57
  (* 
58
59
60
61
    The following definitions and the axiom Dirichlet 
    (provable by natural induction) are necessary to
    prove the lemma Inter6, which is sufficient for
    the proof of WPs for the function [set] below.
62
  *)
63

64
  logic permutation (n : int) (a : array int) =
65
    (forall i : int. 0 <= i < n -> 0 <= a#i < n) and
66
    (forall i j : int. 0 <= i < j < n -> a#i <> a#j)
67

68
  logic dirichlet (n : int) (a : array int) (i : int) : int
69
70
71

  axiom Dirichlet :
    forall n : int. 
72
    forall a : array int.
73
        permutation n a ->
74
        (forall i : int. 0 <= i < n -> 
75
76
            0 <= dirichlet n a i < n and 
            a # dirichlet n a i = i)
77
78

  lemma Inter6 :
79
    forall a : sparse_array . invariant a -> 
80
        let (SA val idx back sz n) = a in
81
        n = sz -> 
82
            permutation sz back /\
83
            forall i : int. 0 <= i < sz ->
84
                idx#i = dirichlet sz back i /\ is_elt a i
85
86
87
88
89
90
91
}


(*
parameter create :
  sz:int -> 
  { 0 <= sz <= maxlen } 
92
  ref sparse_array
93
  { sa_sz !result = sz and forall i:int. model !result i = default }
94
95
*)

96
parameter malloc : n:int -> {} array 'a { A.length result = n }
97
98
99

let create sz =
  { 0 <= sz <= maxlen } 
100
  ref (SA (malloc sz) (malloc sz) (malloc sz) sz 0)
101
102
  { invariant !result and 
    sa_sz !result = sz and forall i:int. model !result i = default }
103
104

let test a i =
105
  { 0 <= i < sa_sz !a }
106
107
108
  let idx = sa_idx !a in
  let back = sa_back !a in
  let n = sa_n !a in
109
110
  0 <= A.select idx i && A.select idx i < n &&
  A.select back (A.select idx i) = i
111
  { result=True <-> is_elt !a i }
112
113
114

(*
parameter get : 
115
  a:ref sparse_array -> i:int -> 
116
    { 0 <= i < sa_sz !a } 
117
    elt reads a
118
    { result = model !a i }
119
120
*)
let get a i =
121
  { 0 <= i < sa_sz !a and invariant !a } 
122
123
124
125
126
  let val = sa_val !a in
  if test a i then
    A.select val i 
  else
    default
127
  { result = model !a i }
128
129
130

(*
parameter set :
131
  a:ref sparse_array -> i:int -> v:elt -> 
132
    { 0 <= i < sa_sz !a and invariant !a } 
133
    unit writes a 
134
135
136
137
    { invariant !a and 
      sa_sz !a = sa_sz (old !a) and
      model !a i = v and
      forall j:int. j <> i -> model !a j = model (old !a) j }
138
139
*)
let set a i v =
140
  { 0 <= i < sa_sz !a and invariant !a } 
141
  (* let SA val idx back sz n = !a in *)
142
143
144
145
146
147
148
  let val = sa_val !a in
  let idx = sa_idx !a in
  let back = sa_back !a in
  let sz= sa_sz !a in
  let n = sa_n !a in
  let val = A.store val i v in
  if test a i then
149
    a := SA val idx back sz n
150
151
152
153
  else begin
    assert { n < sz };
    let idx = A.store idx i n in 
    let back = A.store back n i in
154
    a := SA val idx back sz (n+1)
155
  end
156
157
158
159
  { invariant !a and 
    sa_sz !a = sa_sz (old !a) and
    model !a i = v and
    forall j:int. j <> i -> model !a j = model (old !a) j }
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179

let harness () =
  let a = create 10 in
  let b = create 20 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_0 = get a 0 in assert { get_a_0 = default };
  let get_b_0 = get b 0 in assert { get_b_0 = default };
  ()


(*
Local Variables: 
compile-command: "unset LANG; make -C ../.. examples/programs/vacid_0_sparse_array"
End: 
*)