why3/examples/resizable_array.mlw

module ResizableArraySpec

  use int.Int
  use map.Map
  use map.Const

  type rarray 'a = private {
    ghost mutable length: int;
    ghost mutable data: map int 'a
  }

  function ([]) (r: rarray 'a) (i: int) : 'a = Map.get r.data i
  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 }

  val make (len: int) (dummy: 'a) : rarray 'a
    requires { 0 <= len }
    ensures  { result.length = len }
    ensures  { result.data = Const.const dummy }
    (* 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 writes {r}
    requires { 0 <= i < r.length } ensures { r = (old r)[i <- v] }

  val resize (r: rarray 'a) (len: int) : unit writes {r}
    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 writes {r1}
    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 *)

  use int.Int
  use int.MinMax
  use array.Array as A

  type rarray 'a =
    { dummy: 'a; mutable length: int; mutable data: A.array 'a }
    invariant { 0 <= length <= A.length data }
    invariant { forall i: int. length <= i < A.length data ->
                  A.([]) data i = dummy }
    by { dummy = any 'a; length = 0; data = A.make 0 (any 'a) }

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

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

  let make (len: int) (dummy: 'a) : rarray 'a
    requires { 0 <= len }
    ensures { result.dummy = dummy }
    ensures { result.length = len }
    ensures { forall i:int. 0 <= i < len -> A.([]) result.data i = dummy }
    =
    { dummy = dummy; length = len; data = A.make len dummy }

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

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

  let 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] }
    =
    let n = A.length r.data in
    if len > n then begin
      let a = A.make (max len (2 * n)) r.dummy in
      A.blit r.data 0 a 0 n;
      r.data <- a
    end else begin
      A.fill r.data len (n - len) r.dummy
    end;
    r.length <- len

  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
    resize r1 (length r1 + length r2);
    A.blit r2.data 0 r1.data n1 (length r2)

  (* 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 int.Int
  use ResizableArrayImplem

  let test1 () =
    let r = make 10 0 in
    assert { r.length = 10 };
    r[0] <- 17;
    resize r 7;
    assert { r[0] = 17 };
    assert { r.length = 7 }

  let test2 () =
    let r1 = make 10 0 in
    r1[0] <- 17;
    let r2 = make 10 0 in
    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 };
    ()

end