Insertion in sorted binary tree

  • fully automatic (with redefinition of sorted tree)
  • old def was using lists

    module Bintree_insert
    
      use import bintree.Tree
      use import bintree.Size
      use import bintree.Inorder
      use import bintree.InorderLength
      use import int.Int
    (*-------------------------------*)
    predicate memt (t : tree int) (k : int) =
        match t with
        | Empty -> false
        | Node t1 x t2 -> (k = x) \/ memt t1 k \/ memt t2 k
        end
    
      predicate leq_tree (x : int) (t : tree int) =
        forall k : int. memt t k -> k <= x
    
      predicate geq_tree (x : int) (t : tree int) =
        forall k : int. memt t k -> x <= k
    
      predicate sorted (t : tree int) =
        match t with
        | Empty -> true
        | Node t1 x t2 -> sorted t1 /\ sorted t2 /\ leq_tree x t1 /\ geq_tree x t2
        end
    (*-------------------------------*)
    
      let rec add (t : tree int) (v : int) : tree int =
        requires {sorted t}
        ensures {(sorted result) /\ (forall x : int. memt result x -> (memt t x \/ x = v)) }
        match t with
         | Empty -> Node (Empty) v (Empty)
         | Node t1 x t2 ->
           if v <= x then Node (add t1 v) x t2 else Node t1 x (add t2 v)
        end
    
    end
    

  • Generated by why3doc 0.85