## Resizable arrays

Demonstration of Why3 nested mutable structures

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

```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
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 *)

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
```