array.mlw 7.32 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
(** {1 Arrays} *)
2

MARCHE Claude's avatar
MARCHE Claude committed
3 4
(** {2 Generic Arrays}

5 6
The length is a non-mutable field, so that we get for free that
modification of an array does not modify its length.
MARCHE Claude's avatar
MARCHE Claude committed
7 8

*)
9

10 11 12
module Array

  use import int.Int
13
  use import map.Map as M
14

15
  type array 'a model { length : int; mutable elts : map int 'a }
16
    invariant { 0 <= self.length }
17

Andrei Paskevich's avatar
Andrei Paskevich committed
18
  function get (a: array 'a) (i: int) : 'a = M.get a.elts i
19

Andrei Paskevich's avatar
Andrei Paskevich committed
20
  function set (a: array 'a) (i: int) (v: 'a) : array 'a =
21
    { a with elts = M.set a.elts i v }
22

MARCHE Claude's avatar
MARCHE Claude committed
23
  (** syntactic sugar *)
Andrei Paskevich's avatar
Andrei Paskevich committed
24 25
  function ([]) (a: array 'a) (i: int) : 'a = get a i
  function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
26

27 28 29
  val ([]) (a: array 'a) (i: int) : 'a reads {a}
    requires { 0 <= i < length a }
    ensures  { result = a[i] }
30

31 32 33
  val ([]<-) (a: array 'a) (i: int) (v: 'a) : unit writes {a}
    requires { 0 <= i < length a }
    ensures  { a.elts = M.set (old a.elts) i v }
34

35
  val length (a: array 'a) : int ensures { result = a.length }
36

MARCHE Claude's avatar
MARCHE Claude committed
37
  (** unsafe get/set operations with no precondition *)
38 39
  exception OutOfBounds

40 41 42 43
  let defensive_get (a: array 'a) (i: int)
    ensures { 0 <= i < length a /\ result = a[i] }
    raises { OutOfBounds -> i < 0 \/ i >= length a }
  = if i < 0 || i >= length a then raise OutOfBounds;
44
    a[i]
45

46 47 48 49
  let defensive_set (a: array 'a) (i: int) (v: 'a)
    ensures { 0 <= i < length a /\ a = (old a)[i <- v] }
    raises { OutOfBounds -> i < 0 \/ i >= length a }
  = if i < 0 || i >= length a then raise OutOfBounds;
50
    a[i] <- v
51

52
  function make (n: int) (v: 'a) : array 'a =
53 54 55 56 57 58 59 60 61 62 63 64
    { length = n; elts = M.const v }

  val make (n: int) (v: 'a) : array 'a
    requires { n >= 0 } ensures { result = make n v }

  val append (a1: array 'a) (a2: array 'a) : array 'a
    ensures { length result = length a1 + length a2 }
    ensures { forall i:int. 0 <= i < length a1 -> result[i] = a1[i] }
    ensures {
      forall i:int. 0 <= i < length a2 -> result[length a1 + i] = a2[i] }

  val sub (a: array 'a) (ofs: int) (len: int) : array 'a
65
    requires { 0 <= ofs /\ 0 <= len /\ ofs + len <= length a }
66 67 68 69 70 71 72 73
    ensures  { length result = len }
    ensures  { forall i:int. 0 <= i < len -> result[i] = a[ofs + i] }

  val copy (a: array 'a) : array 'a
    ensures  { length result = length a }
    ensures  { forall i:int. 0 <= i < length result -> result[i] = a[i] }

  let fill (a: array 'a) (ofs: int) (len: int) (v: 'a)
74
    requires { 0 <= ofs /\ 0 <= len /\ ofs + len <= length a }
75 76 77 78
    ensures  { forall i:int.
      (0 <= i < ofs \/ ofs + len <= i < length a) -> a[i] = (old a)[i] }
    ensures  { forall i:int. ofs <= i < ofs + len -> a[i] = v }
  = 'Init:
79
    for k = 0 to len - 1 do
80 81 82
      invariant { forall i:int.
        (0 <= i < ofs \/ ofs + len <= i < length a) -> a[i] = (at a 'Init)[i] }
      invariant { forall i:int. ofs <= i < ofs + k -> a[i] = v }
83 84
      a[ofs + k] <- v
    done
85

Andrei Paskevich's avatar
Andrei Paskevich committed
86
  val blit (a1: array 'a) (ofs1: int)
87
                 (a2: array 'a) (ofs2: int) (len: int) : unit writes {a2}
88 89
    requires { 0 <= ofs1 /\ 0 <= len /\ ofs1 + len <= length a1 }
    requires { 0 <= ofs2 /\             ofs2 + len <= length a2 }
90 91 92 93
    ensures  { forall i:int.
      (0 <= i < ofs2 \/ ofs2 + len <= i < length a2) -> a2[i] = (old a2)[i] }
    ensures  { forall i:int.
      ofs2 <= i < ofs2 + len -> a2[i] = a1[ofs1 + i - ofs2] }
94

MARCHE Claude's avatar
MARCHE Claude committed
95
  (*** TODO?
96 97
     - concat : 'a array list -> 'a array
     - to_list
98
     - of_list
99
  *)
100 101 102

end

MARCHE Claude's avatar
MARCHE Claude committed
103 104
(** {2 Sorted Arrays} *)

105 106
module ArraySorted

107
  use import int.Int
108
  use import Array
Andrei Paskevich's avatar
Andrei Paskevich committed
109
  clone import map.MapSorted as M with type elt = int, predicate le = (<=)
110

Andrei Paskevich's avatar
Andrei Paskevich committed
111
  predicate sorted_sub (a : array int) (l u : int) =
112 113
    M.sorted_sub a.elts l u

Andrei Paskevich's avatar
Andrei Paskevich committed
114
  predicate sorted (a : array int) =
115 116 117 118
    M.sorted_sub a.elts 0 a.length

end

MARCHE Claude's avatar
MARCHE Claude committed
119 120
(** {2 Arrays Equality} *)

121 122
module ArrayEq

123
  use import Array
124
  use import map.MapEq as M
125

Andrei Paskevich's avatar
Andrei Paskevich committed
126
  predicate array_eq_sub (a1 a2: array 'a) (l u: int) =
127 128
    map_eq_sub a1.elts a2.elts l u

Andrei Paskevich's avatar
Andrei Paskevich committed
129 130
  predicate array_eq (a1 a2: array 'a) =
    a1.length = a2.length /\
131 132 133 134
    array_eq_sub a1 a2 0 a1.length

end

MARCHE Claude's avatar
MARCHE Claude committed
135 136
(** {2 Permutation} *)

137 138
module ArrayPermut

139
  use import int.Int
140
  use import Array
141
  use import map.MapPermut as M
142

Andrei Paskevich's avatar
Andrei Paskevich committed
143
  predicate exchange (a1 a2: array 'a) (i j: int) =
144 145
    M.exchange a1.elts a2.elts i j

Andrei Paskevich's avatar
Andrei Paskevich committed
146
  predicate permut_sub (a1 a2: array 'a) (l u: int) =
147 148
    M.permut_sub a1.elts a2.elts l u

Andrei Paskevich's avatar
Andrei Paskevich committed
149 150
  predicate permut (a1 a2: array 'a) =
    a1.length = a2.length /\ M.permut_sub a1.elts a2.elts 0 a1.length
151

152
  lemma exchange_permut:
153
    forall a1 a2: array 'a, i j: int [exchange a1 a2 i j].
154 155 156 157
    exchange a1 a2 i j -> a1.length = a2.length ->
    0 <= i < a1.length -> 0 <= j < a1.length ->
    permut a1 a2

158 159 160 161 162 163 164 165
  lemma permut_sym:
    forall a1 a2: array 'a.
    permut a1 a2 -> permut a2 a1

  lemma permut_trans:
    forall a1 a2 a3: array 'a.
    permut a1 a2 -> permut a2 a3 -> permut a1 a3

166
  use import ArrayEq
167 168 169 170 171 172 173 174 175

  lemma array_eq_sub_permut:
    forall a1 a2: array 'a, l u: int.
    array_eq_sub a1 a2 l u -> permut_sub a1 a2 l u

  lemma array_eq_permut:
    forall a1 a2: array 'a.
    array_eq a1 a2 -> permut a1 a2

176 177
end

MARCHE Claude's avatar
MARCHE Claude committed
178 179
(** {2 Sum of elements} *)

180 181
module ArraySum

182
  use import Array
183
  use import map.MapSum as M
184

MARCHE Claude's avatar
MARCHE Claude committed
185
  (** [sum a l h] is the sum of [a[i]] for [l <= i < h] *)
Andrei Paskevich's avatar
Andrei Paskevich committed
186
  function sum (a: array int) (l h: int) : int = M.sum a.elts l h
187 188 189

end

190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208
(** {2 Number of array elements satisfying a given predicate}

This module is parametrized by a predicate [pr]. It is supposed to be
cloned with needed instances for [pr]. It is also parametrized by a
type [param] to be used as an additional parameter to [pr].

*)

module NumOfParam
  use import Array

  type elt
  type param
  predicate pr (p: param) (i: int) (e: elt)

  type param_ = (array elt, param)
  predicate pr_ (p: param_) (i: int) = let (a, p) = p in pr p i a[i]
  clone import int.NumOfParam with type param = param_, predicate pr = pr_

209
  (** the number of a[i] such that [l <= i < u] and [pr p i a[i]] *)
210 211 212
  function numof (a: array elt) (p: param) (l u: int) : int = num_of (a, p) l u
end

213 214 215 216 217 218 219 220 221 222 223 224 225 226
(** the number of a[i] such that [l <= i < u] and [a[i] = v] *)
module NumOfEq
  use import Array

  type elt

  type param = (array elt, elt)
  predicate pr (p: param) (i: int) = let (a, v) = p in a[i] = v
  clone import int.NumOfParam with type param = param, predicate pr = pr

  function numof (a: array elt) (v: elt) (l u: int) : int = num_of (a, v) l u
end

(** the number of a[i] such that [l <= i < u] and [pr i a[i]] *)
227 228 229 230 231 232 233 234 235 236 237 238 239
module NumOf
  use import Array

  type elt
  predicate pr (i: int) (e: elt)

  type param = array elt
  predicate pr_ (a: param) (i: int) = pr i a[i]
  clone import int.NumOfParam with type param = param, predicate pr = pr_

  function numof (a: array elt) (l u: int) : int = num_of a l u
end

240 241 242
module TestArray

  use import int.Int
243
  use import Array
244

245
  let test_append () =
246 247
    let a1 = make 17 2 in
    assert { a1[3] = 2 };
248
    a1[3] <- 4;
249 250 251 252 253 254 255 256 257
    assert { a1[3] = 4 };
    let a2 = make 25 3 in
    assert { a2[0] = 3 }; (* needed to prove a[17]=3 below *)
    let a  = append a1 a2 in
    assert { length a = 42 };
    assert { a[3] = 4 };
    assert { a[17] = 3 };
    ()

258
  let test_fill () =
259 260
    let a = make 17 True in
    fill a 10 4 False;
261 262 263
    assert { a[9] = True };
    assert { a[10] = False };
    assert { a[14] = True }
264

265 266 267 268 269 270 271 272 273 274
  let test_blit () =
    let a1 = make 17 True in
    let a2 = make 25 False in
    blit a1 10 a2 17 7;
    assert { a1[10] = True  };
    assert { a2[16] = False };
    assert { a2[17] = True  };
    assert { a2[23] = True  };
    assert { a2[24] = False }

275
end