## Snapshotable Trees

Formalized Verification of Snapshotable Trees: Separation and Sharing Hannes Mehnert, Filip Sieczkowski, Lars Birkedal, and Peter Sestoft VSTTE 2012

Authors: Jean-Christophe Filliâtre

Topics: Trees

Tools: Why3

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

```(*
Snapshotable Trees

Formalized Verification of Snapshotable Trees: Separation and Sharing
Hannes Mehnert, Filip Sieczkowski, Lars Birkedal, and Peter Sestoft
VSTTE 2012
*)

(* Purely applicative binary trees with elements at the nodes *)

theory Tree

use export int.Int
use export list.List
use export list.Length
use export list.Append

type elt = int

type tree =
| Empty
| Node tree elt tree

function tree_elements (t: tree) : list elt = match t with
| Empty -> Nil
| Node l x r -> tree_elements l ++ Cons x (tree_elements r)
end

predicate mem (x: elt) (t: tree) = match t with
| Empty -> false
| Node l y r -> mem x l || x = y || mem x r
end

end

(* Purely applicative iterators over binary trees *)

module Enum

use Tree

type enum =
| Done
| Next elt tree enum

function enum_elements (e: enum) : list elt = match e with
| Done -> Nil
| Next x r e -> Cons x (tree_elements r ++ enum_elements e)
end

let rec enum t e variant {t}
ensures { enum_elements result = tree_elements t ++ enum_elements e }
= match t with
| Empty -> e
| Node l x r -> enum l (Next x r e)
end

end

(* Mutable iterators with a Java-like API *)

module Iterator

use Tree
use Enum

type iterator = { mutable it: enum }

function elements (i: iterator) : list elt = enum_elements i.it

let create_iterator (t: tree)
ensures { elements result = tree_elements t }
= { it = enum t Done }

predicate hasNext (i: iterator) = i.it <> Done

let hasNext (i: iterator)
ensures { result = True <-> hasNext i }
= match i.it with Done -> False | _ -> True end

let next (i: iterator)
requires { hasNext i }
ensures { old (elements i) = Cons result (elements i) }
= match i.it with
| Done -> absurd
| Next x r e -> i.it <- enum r e; x
end

end

(* Binary search trees *)

module BSTree

use export Tree

predicate lt_tree (x: elt) (t: tree) =
forall y: elt. mem y t -> y < x

predicate gt_tree (x: elt) (t: tree) =
forall y: elt. mem y t -> x < y

predicate bst (t: tree) =
match t with
| Empty -> true
| Node l x r -> bst l /\ bst r /\ lt_tree x l /\ gt_tree x r
end

let rec bst_mem (x: elt) (t: tree)
requires { bst t } ensures { result=True <-> mem x t } variant { t }
= match t with
| Empty ->
False
| Node l y r ->
if x < y then bst_mem x l else x = y || bst_mem x r
end

let rec bst_add (x: elt) (t: tree)
requires { bst t }
ensures { bst result /\ not (mem x t) /\
forall y: elt. mem y result <-> y=x || mem y t }
raises { Already -> mem x t }
variant { t }
= match t with
| Empty ->
Node Empty x Empty
| Node l y r ->
if x = y then raise Already;
if x < y then Node (bst_add x l) y r else Node l y (bst_add x r)
end

end

(* Imperative trees with add/contains/snapshot/iterator API *)

module ITree

use export BSTree
use export Iterator

type itree = { mutable tree: tree } invariant { bst tree }

let create () = { tree = Empty }

let contains (t: itree) (x: elt)
ensures { result=True <-> mem x t.tree }
= bst_mem x t.tree

let add (t: itree) (x: elt)
ensures { (result=False <-> mem x (old t.tree)) /\
forall y: elt. mem y t.tree <-> y=x || mem y (old t.tree) }
= try t.tree <- bst_add x t.tree; True with Already -> False end

let snapshot (t: itree) = { tree = t.tree }

let iterator (t: itree)
ensures { elements result = tree_elements t.tree }
= create_iterator t.tree

end

module Harness

use ITree

let test () =
let t = create () in
let _ = add t 1 in
let _ = add t 2 in
let _ = add t 3 in
assert { mem 2 t.tree };
let s = snapshot t in
let it = iterator s in
while hasNext it do
invariant { bst t.tree }
variant { length (elements it) }
let x = next it in
let _ = add t (x * 3) in
()
done

end
```