## Flexible Arrays

Flexible arrays implemented with Braun trees

Authors: Jean-Christophe Filliâtre

Tools: Why3

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

Flexible arrays implemented with Braun trees.

References: - W. Braun, M. Rem, A logarithmic implementation of flexible arrays. Memorandum MR83/4. Eindhoven University of Technology. 1983. - Hoogerwoord, R. R. A logarithmic implementation of flexible arrays. Conference on Mathematics of Program Construction. 1992. - Chris Okasaki. Three Algorithms on Braun Trees (Functional Pearl) J. Functional Programming 7 (6) 661–666. 1997

See also braun_trees.mlw for an implementation of priority queues using Braun trees (and a proof that a Braun tree has logarithmic height).

Author: Jean-Christophe Filliâtre (CNRS)

First, we work on bare Braun trees

```module BraunTrees

use int.Int
use int.ComputerDivision
use export bintree.Tree
use export bintree.Size
use seq.Seq

predicate braun (t: tree 'a) = match t with
| Empty      -> true
| Node l _ r -> (size l = size r || size l = size r + 1) && braun l && braun r
end

let rec function get_tree (t: tree 'a) (i: int) : 'a
requires { 0 <= i < size t }
requires { braun t }
variant  { t }
= match t with
| Empty -> absurd
| Node l x r ->
if i = 0 then x else
if mod i 2 = 1 then get_tree l (div i 2) else get_tree r (div i 2 - 1)
end

let rec function set_tree (t: tree 'a) (i: int) (v: 'a) : (r: tree 'a)
requires { 0 <= i < size t }
requires { braun t }
variant  { t }
ensures  { size r = size t }
ensures  { braun r }
ensures  { get_tree r i = v }
ensures  { forall j. 0 <= j < t.size -> j<>i -> get_tree r j = get_tree t j }
= match t with
| Empty -> absurd
| Node l x r ->
if i = 0 then Node l v r else
if mod i 2 = 1 then Node (set_tree l (div i 2) v) x r
else Node l x (set_tree r (div i 2 - 1) v)
end

let rec make_tree2 (n: int) (v: 'a) : (l: tree 'a, r: tree 'a)
requires { n >= 0}
variant { n }
ensures { size l = n+1 && size r = n }
ensures { braun l && braun r }
ensures { forall i. 0 <= i < size l -> get_tree l i = v }
ensures { forall i. 0 <= i < size r -> get_tree r i = v }
= if n = 0 then
Node Empty v Empty, Empty
else if mod n 2 = 1 then
let l, r = make_tree2 (div n 2) v in
Node l v r, Node r v r
else
let l, r = make_tree2 (div n 2 - 1) v in
Node l v l, Node l v r

let make_tree (n: int) (v: 'a) : (r: tree 'a)
requires { n >= 0}
ensures  { size r = n }
ensures  { braun r }
ensures  { forall i. 0 <= i < size r -> get_tree r i = v }
= let _, r = make_tree2 n v in r

(* left insertion/removal *)

let rec cons_tree (v: 'a) (t: tree 'a) : (r: tree 'a)
requires { braun t }
variant  { t }
ensures  { size r = size t + 1 }
ensures  { braun r }
ensures  { get_tree r 0 = v }
ensures  { forall i. 0 <= i < size t -> get_tree r (i+1) = get_tree t i }
= match t with
| Empty      -> Node Empty v Empty
| Node l x r -> Node (cons_tree x r) v l
end

let rec tail_tree (t: tree 'a) : (r: tree 'a)
requires { braun t }
requires { size t > 0 }
variant  { t }
ensures  { size r = size t - 1 }
ensures  { braun r }
ensures  { forall i. 0 < i < size t -> get_tree r (i-1) = get_tree t i }
= match t with
| Empty              -> absurd
| Node Empty _ Empty -> Empty
| Node l     _ r     -> Node r (get_tree l 0) (tail_tree l)
end

(* right insertion/removal *)

let rec snoc_tree (s: int) (t: tree 'a) (v: 'a) : (r: tree 'a)
requires { braun t }
requires { s = size t }
variant  { t }
ensures  { size r = size t + 1 }
ensures  { braun r }
ensures  { forall i. 0 <= i < size t -> get_tree r i = get_tree t i }
ensures  { get_tree r s = v }
= match t with
| Empty      -> Node Empty v Empty
| Node l x r -> if mod s 2 = 1 then Node (snoc_tree (div s 2) l v) x r
else Node l x (snoc_tree (div s 2 - 1) r v)
end

let rec liat_tree (s: int) (t: tree 'a) : (r: tree 'a)
requires { braun t }
requires { s = size t > 0 }
variant  { t }
ensures  { size r = size t - 1 }
ensures  { braun r }
ensures  { forall i. 0 <= i < size r -> get_tree r i = get_tree t i }
= match t with
| Empty -> absurd
| Node Empty _ Empty -> Empty
| Node l     x r     -> if mod s 2 = 0 then Node (liat_tree (div s 2) l) x r
else Node l x (liat_tree (div s 2) r)
end

(* TODO: Okasaki's of_list *)

end

```

Second, we encapsulate Braun trees in a record, together with its size and suitable invariants.

```module FlexibleArrays

use int.Int
use BraunTrees as B

type t 'a = {
size: int;
tree: B.tree 'a;
}
invariant { B.braun tree }
invariant { B.size tree = size >= 0 }

let constant empty : t 'a
= { size = 0; tree = B.Empty }
ensures { result.size = 0 }

let function get (t: t 'a) (i: int) : 'a
requires { 0 <= i < t.size }
= B.get_tree t.tree i

let set (t: t 'a) (i: int) (v: 'a) : (r: t 'a)
requires { 0 <= i < t.size }
ensures  { r.size = t.size }
ensures  { get r i = v }
ensures  { forall j. 0 <= j < t.size -> j<>i -> get r j = get t j }
= { size = t.size; tree = B.set_tree t.tree i v }

let make_tree (n: int) (v: 'a) : (r: t 'a)
requires { n >= 0}
ensures  { r.size = n }
ensures  { forall i. 0 <= i < r.size -> get r i = v }
= { size = n; tree = B.make_tree n v }

(* left insertion/removal *)

let cons (v: 'a) (t: t 'a) : (r: t 'a)
ensures  { size r = size t + 1 }
ensures  { get r 0 = v }
ensures  { forall i. 0 <= i < t.size -> get r (i+1) = get t i }
= { size = t.size + 1; tree = B.cons_tree v t.tree }

let tail (t: t 'a) : (r: t 'a)
requires { t.size > 0 }
ensures  { r.size = t.size - 1 }
ensures  { forall i. 0 < i < size t -> get r (i-1) = get t i }
= { size = t.size - 1; tree = B.tail_tree t.tree }

(* right insertion/removal *)

let snoc (t: t 'a) (v: 'a) : (r: t 'a)
ensures  { r.size = t.size + 1 }
ensures  { forall i. 0 <= i < t.size -> get r i = get t i }
ensures  { get r t.size = v }
= { size = t.size + 1; tree = B.snoc_tree t.size t.tree v }

let liat (t: t 'a) : (r: t 'a)
requires { t.size > 0 }
ensures  { r.size = t.size - 1 }
ensures  { forall i. 0 <= i < r.size -> get r i = get t i }
= { size = t.size - 1; tree = B.liat_tree t.size t.tree }

end
```