Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
26
  val ([]) (a: array 'a) (i: int) :
27
    { 0 <= i < length a } 'a reads a { result = a[i] }
28

Andrei Paskevich's avatar
Andrei Paskevich committed
29
  val ([]<-) (a: array 'a) (i: int) (v: 'a) :
30
    { 0 <= i < length a } unit writes a { a.elts = M.set (old a.elts) i v }
31

Andrei Paskevich's avatar
Andrei Paskevich committed
32
  val length (a: array 'a) : {} int { result = a.length }
33

MARCHE Claude's avatar
MARCHE Claude committed
34
  (** unsafe get/set operations with no precondition *)
35 36
  exception OutOfBounds

37
  let defensive_get (a: array 'a) (i: int) =
38
    { }
39 40
    if i < 0 || i >= length a then raise OutOfBounds;
    a[i]
Andrei Paskevich's avatar
Andrei Paskevich committed
41 42
    { 0 <= i < length a /\ result = a[i] }
    | OutOfBounds -> { i < 0 \/ i >= length a }
43

44
  let defensive_set (a: array 'a) (i: int) (v: 'a) =
45
    { }
46 47
    if i < 0 || i >= length a then raise OutOfBounds;
    a[i] <- v
Andrei Paskevich's avatar
Andrei Paskevich committed
48 49
    { 0 <= i < length a /\ a = (old a)[i <- v] }
    | OutOfBounds -> { i < 0 \/ i >= length a }
50

Andrei Paskevich's avatar
Andrei Paskevich committed
51
  val make (n: int) (v: 'a) :
52
    { n >= 0 }
53
    array 'a
54
    { result = {| length = n; elts = M.const v |} }
MARCHE Claude's avatar
MARCHE Claude committed
55
     (*** { length result = n /\ forall i:int. 0 <= i < n -> result[i] = v} *)
56

Andrei Paskevich's avatar
Andrei Paskevich committed
57
  val append (a1: array 'a) (a2: array 'a) :
58 59
    {}
    array 'a
Andrei Paskevich's avatar
Andrei Paskevich committed
60 61
    { length result = length a1 + length a2 /\
      (forall i:int. 0 <= i < length a1 -> result[i] = a1[i]) /\
62 63
      (forall i:int. 0 <= i < length a2 -> result[length a1 + i] = a2[i]) }

Andrei Paskevich's avatar
Andrei Paskevich committed
64
  val sub (a: array 'a) (ofs: int) (len: int) :
Andrei Paskevich's avatar
Andrei Paskevich committed
65
    { 0 <= ofs /\ ofs + len <= length a }
66
    array 'a
Andrei Paskevich's avatar
Andrei Paskevich committed
67
    { length result = len /\
68 69
      forall i:int. 0 <= i < len -> result[i] = a[ofs + i] }

Andrei Paskevich's avatar
Andrei Paskevich committed
70
  val copy (a: array 'a) :
71 72
    {}
    array 'a
Andrei Paskevich's avatar
Andrei Paskevich committed
73
    { length result = length a /\
74 75
      forall i:int. 0 <= i < length result -> result[i] = a[i] }

76
  let fill (a: array 'a) (ofs: int) (len: int) (v: 'a) =
Andrei Paskevich's avatar
Andrei Paskevich committed
77
    { 0 <= ofs /\ ofs + len <= length a }
78
'Init:
79 80 81
    for k = 0 to len - 1 do
      invariant {
        (forall i:int.
82
        (0 <= i < ofs \/ ofs + len <= i < length a) -> a[i] = (at a 'Init)[i])
Andrei Paskevich's avatar
Andrei Paskevich committed
83
        /\
84 85 86 87 88
        (forall i:int. ofs <= i < ofs + k -> a[i] = v)
      }
      a[ofs + k] <- v
    done
    { (forall i:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
89 90
        (0 <= i < ofs \/ ofs + len <= i < length a) -> a[i] = (old a)[i])
      /\
91 92
      (forall i:int.
        ofs <= i < ofs + len -> a[i] = v) }
93

Andrei Paskevich's avatar
Andrei Paskevich committed
94
  val blit (a1: array 'a) (ofs1: int)
95
                 (a2: array 'a) (ofs2: int) (len: int) :
Andrei Paskevich's avatar
Andrei Paskevich committed
96 97
    { 0 <= ofs1 /\ ofs1 + len <= length a1 /\
      0 <= ofs2 /\ ofs2 + len <= length a2 }
98 99 100
    unit
    writes a2
    { (forall i:int.
Andrei Paskevich's avatar
Andrei Paskevich committed
101 102
        (0 <= i < ofs2 \/ ofs2 + len <= i < length a2) -> a2[i] = (old a2)[i])
      /\
103 104
      (forall i:int.
        ofs2 <= i < ofs2 + len -> a2[i] = a1[ofs1 + i - ofs2]) }
105

MARCHE Claude's avatar
MARCHE Claude committed
106
  (*** TODO?
107 108
     - concat : 'a array list -> 'a array
     - to_list
109
     - of_list
110
  *)
111 112 113

end

MARCHE Claude's avatar
MARCHE Claude committed
114 115
(** {2 Sorted Arrays} *)

116 117
module ArraySorted

118
  use import int.Int
119
  use import module Array
Andrei Paskevich's avatar
Andrei Paskevich committed
120
  clone import map.MapSorted as M with type elt = int, predicate le = (<=)
121

Andrei Paskevich's avatar
Andrei Paskevich committed
122
  predicate sorted_sub (a : array int) (l u : int) =
123 124
    M.sorted_sub a.elts l u

Andrei Paskevich's avatar
Andrei Paskevich committed
125
  predicate sorted (a : array int) =
126 127 128 129
    M.sorted_sub a.elts 0 a.length

end

MARCHE Claude's avatar
MARCHE Claude committed
130 131
(** {2 Arrays Equality} *)

132 133 134
module ArrayEq

  use import module Array
135
  use import map.MapEq as M
136

Andrei Paskevich's avatar
Andrei Paskevich committed
137
  predicate array_eq_sub (a1 a2: array 'a) (l u: int) =
138 139
    map_eq_sub a1.elts a2.elts l u

Andrei Paskevich's avatar
Andrei Paskevich committed
140 141
  predicate array_eq (a1 a2: array 'a) =
    a1.length = a2.length /\
142 143 144 145
    array_eq_sub a1 a2 0 a1.length

end

MARCHE Claude's avatar
MARCHE Claude committed
146 147
(** {2 Permutation} *)

148 149
module ArrayPermut

150
  use import int.Int
151 152 153
  use import module Array
  clone import map.MapPermut as M

Andrei Paskevich's avatar
Andrei Paskevich committed
154
  predicate exchange (a1 a2: array 'a) (i j: int) =
155 156
    M.exchange a1.elts a2.elts i j

Andrei Paskevich's avatar
Andrei Paskevich committed
157
  predicate permut_sub (a1 a2: array 'a) (l u: int) =
158 159
    M.permut_sub a1.elts a2.elts l u

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

163
  lemma exchange_permut:
164
    forall a1 a2: array 'a, i j: int [exchange a1 a2 i j].
165 166 167 168
    exchange a1 a2 i j -> a1.length = a2.length ->
    0 <= i < a1.length -> 0 <= j < a1.length ->
    permut a1 a2

169 170 171 172 173 174 175 176
  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

177 178 179 180 181 182 183 184 185 186
  use import module ArrayEq

  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

187 188
end

MARCHE Claude's avatar
MARCHE Claude committed
189 190
(** {2 Sum of elements} *)

191 192 193 194 195
module ArraySum

  use import module Array
  clone import map.MapSum as M

MARCHE Claude's avatar
MARCHE Claude committed
196
  (** [sum a l h] is the sum of [a[i]] for [l <= i < h] *)
Andrei Paskevich's avatar
Andrei Paskevich committed
197
  function sum (a: array int) (l h: int) : int = M.sum a.elts l h
198 199 200

end

201 202 203 204 205
module TestArray

  use import int.Int
  use import module Array

206
  let test_append () =
207 208
    let a1 = make 17 2 in
    assert { a1[3] = 2 };
209
    a1[3] <- 4;
210 211 212 213 214 215 216 217 218
    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 };
    ()

219
  let test_fill () =
220 221
    let a = make 17 True in
    fill a 10 4 False;
222 223 224
    assert { a[9] = True };
    assert { a[10] = False };
    assert { a[14] = True }
225

226 227 228 229 230 231 232 233 234 235
  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 }

236 237
end

MARCHE Claude's avatar
MARCHE Claude committed
238
(***
239
Local Variables:
240
compile-command: "unset LANG; make -C .. modules/array"
241
End:
242
*)