array.mlw 6.84 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

178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195
module ArraySwap

  use import int.Int
  use import Array
  use import ArrayPermut

  let swap (a:array 'a) (i:int) (j:int) : unit
    requires { 0 <= i < length a /\ 0 <= j < length a }
    ensures  { exchange (old a) a i j }
    =
    let v = a[i] in
    begin
      a[i] <- a[j];
      a[j] <- v
    end

end

MARCHE Claude's avatar
MARCHE Claude committed
196 197
(** {2 Sum of elements} *)

198 199
module ArraySum

200
  use import Array
201
  use import map.MapSum as M
202

MARCHE Claude's avatar
MARCHE Claude committed
203
  (** [sum a l h] is the sum of [a[i]] for [l <= i < h] *)
Andrei Paskevich's avatar
Andrei Paskevich committed
204
  function sum (a: array int) (l h: int) : int = M.sum a.elts l h
205 206 207

end

208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226
(** {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_

227
  (** the number of a[i] such that [l <= i < u] and [pr p i a[i]] *)
228 229 230
  function numof (a: array elt) (p: param) (l u: int) : int = num_of (a, p) l u
end

231 232 233 234 235 236 237 238 239 240 241 242 243 244
(** 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]] *)
245 246 247 248 249 250 251 252 253 254 255 256
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