resizable_array.mlw 4.43 KB
Newer Older
1

2 3 4 5
module ResizableArraySpec

  use import int.Int
  use import map.Map
6
  use map.Const
7

8 9 10 11
  type rarray 'a = private {
    ghost mutable length: int;
    ghost mutable data: map int 'a
  }
12 13

  function ([]) (r: rarray 'a) (i: int) : 'a = Map.get r.data i
14 15 16
  val function ([<-]) (r: rarray 'a) (i: int) (v: 'a) : rarray 'a
    ensures { result.length = r.length }
    ensures { result.data = Map.set r.data i v }
17 18 19 20

  val make (len: int) (dummy: 'a) : rarray 'a
    requires { 0 <= len }
    ensures  { result.length = len }
21
    ensures  { result.data = Const.const dummy }
22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
    (* ensures  { forall i: int. 0 <= i < len -> result[i] = dummy } *)

  val ([]) (r: rarray 'a) (i: int) : 'a
    requires { 0 <= i < r.length } ensures { result = r[i] }

  val ([]<-) (r: rarray 'a) (i: int) (v: 'a) : unit
    requires { 0 <= i < r.length } ensures { r = (old r)[i <- v] }

  val resize (r: rarray 'a) (len: int) : unit
    requires { 0 <= len }
    ensures  { r.length = len }
    ensures  { forall i: int.
               0 <= i < old r.length -> i < len -> r[i] = (old r)[i] }

  val append (r1: rarray 'a) (r2: rarray 'a) : unit
    ensures { r1.length = old r1.length + r2.length }
    ensures { forall i: int. 0 <= i < r1.length ->
               (i < old r1.length  -> r1[i] = (old r1)[i]) /\
               (old r1.length <= i -> r1[i] = r2[i - old r1.length]) }

end

module ResizableArrayImplem (* : ResizableArraySpec *)
45 46 47

  use import int.Int
  use import int.MinMax
48
  use array.Array as A
49

50 51
  type rarray 'a =
    { dummy: 'a; mutable length: int; mutable data: A.array 'a }
52 53 54
    invariant { 0 <= length <= A.length data }
    invariant { forall i: int. length <= i < A.length data ->
                  A.([]) data i = dummy }
55

56
  function ([]) (r: rarray 'a) (i: int) : 'a = A.([]) r.data i
57

58 59
(*
function make (len: int) (dummy: 'a) : rarray 'a =
60
    { dummy = dummy; length = len; data = A.make len dummy }
61
*)
62

63
  let make (len: int) (dummy: 'a) : rarray 'a
64 65 66
    requires { 0 <= len }
    ensures { result.dummy = dummy }
    ensures { result.length = len }
67
    ensures { forall i:int. 0 <= i < len -> A.([]) result.data i = dummy }
68 69
    =
    { dummy = dummy; length = len; data = A.make len dummy }
70

71
  let ([]) (r: rarray 'a) (i: int) : 'a
72
    requires { 0 <= i < r.length }
73 74
    =
    A.([]) r.data i
75

76
  let ([]<-) (r: rarray 'a) (i: int) (v: 'a) : unit
77 78
    requires { 0 <= i < r.length }
    ensures { r.data.A.elts = A.M.([<-]) (old r).data.A.elts i v }
79 80
    =
    A.([]<-) r.data i v
81

82
  let resize (r: rarray 'a) (len: int) : unit
83
    requires { 0 <= len }
84 85
    ensures  { r.length = len }
    ensures  { forall i: int.
86
                 0 <= i < old r.length -> i < len -> r[i] = (old r)[i] }
87 88
    =
    let n = A.length r.data in
89
    if len > n then begin
90
      let a = A.make (max len (2 * n)) r.dummy in
91
      A.blit r.data 0 a 0 n;
92
      r.data <- a
93 94
    end else begin
      A.fill r.data len (n - len) r.dummy
95 96 97
    end;
    r.length <- len

98 99 100 101 102 103 104
  let append (r1: rarray 'a) (r2: rarray 'a) : unit
    ensures { r1.length = old r1.length + r2.length }
    ensures { forall i: int. 0 <= i < r1.length ->
               (i < old r1.length  -> r1[i] = (old r1)[i]) /\
               (old r1.length <= i -> r1[i] = r2[i - old r1.length]) }
    =
    let n1 = length r1 in
105 106
    resize r1 (length r1 + length r2);
    A.blit r2.data 0 r1.data n1 (length r2)
107

108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136
  (* sanity checks for WhyML typing system *)

(*
  let test_reset1 (r: rarray) =
    let a = A.make 10 dummy in
    r.data <- a;
    A.([]) a 0 (* <-- we cannot access array a anymore *)

  let test_reset2 (r: rarray) =
     let b = r.data in
     r.data <- A.make 10 dummy;
     let x = A.([]) r.data 0 in (* <-- this is accepted *)
     let y = A.([]) b      0 in (* <-- but we cannot access array b anymore *)
     ()

  (* the same, using resize *)
  let test_reset3 (r: rarray) =
     let c = r.data in
     resize r 10;
     let x = A.([]) r.data 0 in (* <-- this is accepted *)
     let y = A.([]) c      0 in (* <-- but we cannot access array c anymore *)
     ()
*)

end

module Test

  use import int.Int
137
  use import ResizableArrayImplem
138 139

  let test1 () =
140
    let r = make 10 0 in
141 142 143 144 145 146 147
    assert { r.length = 10 };
    r[0] <- 17;
    resize r 7;
    assert { r[0] = 17 };
    assert { r.length = 7 }

  let test2 () =
148
    let r1 = make 10 0 in
149
    r1[0] <- 17;
150
    let r2 = make 10 0 in
151 152 153 154 155 156 157 158 159 160
    r2[0] <- 42;
    append r1 r2;
    assert { r1.length = 20 };
    assert { r1[0] = 17 };
    let x = r1[10] in
    assert { x = 42 };
    let y = r2[0] in
    assert { y = 42 };
    ()

161
end