Computer-Aided Program Development Institute of Computer Science Faculty of Engineering, Christian-Albrechts-University of Kiel

{***********************************************************************}
{* SPECIFICATION OF BINARY TREES                                       *}
{***********************************************************************}
 
type BTREE
  basedon NAT, BOOL
  sort Tree
  cons empty : Tree,
       mk : (Tree,Nat,Tree)Tree
  func left : (Tree)Tree,
       right: (Tree)Tree,
       node : (Tree)Nat,
       isempty : (Tree)Bool
  axioms all (t1,t2 : Tree, n : Nat)
    {1}  left(mk(t1,n,t2)) -> t1,
    {2}  right(mk(t1,n,t2)) -> t2,
    {3}  node(mk(t1,n,t2)) -> n,
    {4}  isempty(empty) -> true,
    {5}  isempty(mk(t1,n,t2)) -> false
endoftype
complete BTREE except left, right, node
noetherian BTREE
display BTREE empty = "<>",
              mk = "<_ _ _>",
              isempty = "_ = <>"

{***********************************************************************}
{* SOME EXTENSIONS OF BINARY TREES                                     *}
{***********************************************************************}
 
type HBTREE
  basedon BTREE, NAT, BOOL
  func max   : (Nat,Nat)Nat,
       hight : (Tree)Nat
  axioms all (t1, t2 : Tree, m, n : Nat)
    {1} le(m,n) = true  =>  max(m,n) -> n,
    {2} le(m,n) = false  =>  max(m,n) -> m,
    {3} hight(empty) -> 0,
    {4} hight(mk(t1,n,t2)) -> succ(max(hight(t1),hight(t2)))
endoftype
noetherian HBTREE

type FBTREE
  basedon BTREE, NAT, BOOL
  func append  : (Tree,Tree)Tree,
       flatten : (Tree)Tree
  axioms all (t, t1, t2 : Tree, n : Nat)
    {1} append(empty,t) -> t,
    {2} append(mk(t1,n,t2),t) -> mk(t1,n,append(t2,t)),
    {3} flatten(empty) -> empty,
    {4} flatten(mk(t1,n,t2))  -> append(mk(empty,n,flatten(t1)),flatten(t2))
endoftype
noetherian HBTREE

{***********************************************************************}
{* SOME EXAMPLE TASKS                                                  *} 
{***********************************************************************}
 
task T1
  basedon HBTREE, BTREE, NAT, BOOL
  unknown t : Tree
  goals   hight(t) = 3
endoftask

task T2
  basedon FBTREE, BTREE, NAT, BOOL
  unknown t : Tree
  goals   flatten(flatten(t)) = flatten(t)
endoftask