Toccata

(*
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

  exception Already
    (* bst_add raises exception Already when the element is already present *)

  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