resizable_array.mlw 4.45 KB
Newer Older
1

2 3
module ResizableArraySpec

4 5 6
  use int.Int
  use map.Map
  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 int.Int
  use 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
    by { dummy = any 'a; length = 0; data = A.make 0 (any 'a) }
56

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

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

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

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

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

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

99 100 101 102 103 104 105
  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
106 107
    resize r1 (length r1 + length r2);
    A.blit r2.data 0 r1.data n1 (length r2)
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

137 138
  use int.Int
  use ResizableArrayImplem
139 140

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

  let test2 () =
149
    let r1 = make 10 0 in
150
    r1[0] <- 17;
151
    let r2 = make 10 0 in
152 153 154 155 156 157 158 159 160 161
    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 };
    ()

162
end