examples/resizable_array.mlw

   1
   2 module ResizableArraySpec
   3
   4   use int.Int
   5   use map.Map
   6   use map.Const
   7
   8   type rarray 'a = private {
   9     ghost mutable length: int;
  10     ghost mutable data: map int 'a
  11   }
  12
  13   function ([]) (r: rarray 'a) (i: int) : 'a = Map.get r.data i
  14   val function ([<-]) (r: rarray 'a) (i: int) (v: 'a) : rarray 'a
  15     ensures { result.length = r.length }
  16     ensures { result.data = Map.set r.data i v }
  17
  18   val make (len: int) (dummy: 'a) : rarray 'a
  19     requires { 0 <= len }
  20     ensures  { result.length = len }
  21     ensures  { result.data = Const.const dummy }
  22     (* ensures  { forall i: int. 0 <= i < len -> result[i] = dummy } *)
  23
  24   val ([]) (r: rarray 'a) (i: int) : 'a
  25     requires { 0 <= i < r.length } ensures { result = r[i] }
  26
  27   val ([]<-) (r: rarray 'a) (i: int) (v: 'a) : unit writes {r}
  28     requires { 0 <= i < r.length } ensures { r = (old r)[i <- v] }
  29
  30   val resize (r: rarray 'a) (len: int) : unit writes {r}
  31     requires { 0 <= len }
  32     ensures  { r.length = len }
  33     ensures  { forall i: int.
  34                0 <= i < old r.length -> i < len -> r[i] = (old r)[i] }
  35
  36   val append (r1: rarray 'a) (r2: rarray 'a) : unit writes {r1}
  37     ensures { r1.length = (old r1.length) + r2.length }
  38     ensures { forall i: int. 0 <= i < r1.length ->
  39                (i < old r1.length  -> r1[i] = (old r1)[i]) /\
  40                (old r1.length <= i -> r1[i] = r2[i - old r1.length]) }
  41
  42 end
  43
  44 module ResizableArrayImplem (* : ResizableArraySpec *)
  45
  46   use int.Int
  47   use int.MinMax
  48   use array.Array as A
  49
  50   type rarray 'a =
  51     { dummy: 'a; mutable length: int; mutable data: A.array 'a }
  52     invariant { 0 <= length <= A.length data }
  53     invariant { forall i: int. length <= i < A.length data ->
  54                   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     requires { 0 <= len }
  66     ensures { result.dummy = dummy }
  67     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     ensures  { r.length = len }
  86     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     end else begin
  95       A.fill r.data len (n - len) r.dummy
  96     end;
  97     r.length <- len
  98
  99   let append (r1: rarray 'a) (r2: rarray 'a) : unit
 100     ensures { r1.length = old r1.length + r2.length }
 101     ensures { forall i: int. 0 <= i < r1.length ->
 102                (i < old r1.length  -> r1[i] = (old r1)[i]) /\
 103                (old r1.length <= i -> r1[i] = r2[i - old r1.length]) }
 104     =
 105     let n1 = length r1 in
 106     resize r1 (length r1 + length r2);
 107     A.blit r2.data 0 r1.data n1 (length r2)
 108
 109   (* sanity checks for WhyML typing system *)
 110
 111 (*
 112   let test_reset1 (r: rarray) =
 113     let a = A.make 10 dummy in
 114     r.data <- a;
 115     A.([]) a 0 (* <-- we cannot access array a anymore *)
 116
 117   let test_reset2 (r: rarray) =
 118      let b = r.data in
 119      r.data <- A.make 10 dummy;
 120      let x = A.([]) r.data 0 in (* <-- this is accepted *)
 121      let y = A.([]) b      0 in (* <-- but we cannot access array b anymore *)
 122      ()
 123
 124   (* the same, using resize *)
 125   let test_reset3 (r: rarray) =
 126      let c = r.data in
 127      resize r 10;
 128      let x = A.([]) r.data 0 in (* <-- this is accepted *)
 129      let y = A.([]) c      0 in (* <-- but we cannot access array c anymore *)
 130      ()
 131 *)
 132
 133 end
 134
 135 module Test
 136
 137   use int.Int
 138   use ResizableArrayImplem
 139
 140   let test1 () =
 141     let r = make 10 0 in
 142     assert { r.length = 10 };
 143     r[0] <- 17;
 144     resize r 7;
 145     assert { r[0] = 17 };
 146     assert { r.length = 7 }
 147
 148   let test2 () =
 149     let r1 = make 10 0 in
 150     r1[0] <- 17;
 151     let r2 = make 10 0 in
 152     r2[0] <- 42;
 153     append r1 r2;
 154     assert { r1.length = 20 };
 155     assert { r1[0] = 17 };
 156     let x = r1[10] in
 157     assert { x = 42 };
 158     let y = r2[0] in
 159     assert { y = 42 };
 160     ()
 161
 162 end