[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Tree height



Hello,
 
I am new to PVS and I have a question about Recursive functions. I want to model a binary tree (unsorted) including functions to compute the height of the tree.
 
So I get the following Datatype:
 
binary_tree: datatype
begin
  leaf (val:nat): leaf?
  node(val:nat, left:binary_tree, right:binary_tree): node?
end binary_tree
 
and the theory:
 
bt: theory
begin
  importing binary_tree_adt
  height(T:binary_tree): recursive nat =
  cases T of
    leaf: 0,
    node(v,l,r): if height(l) > height(r) then height(l) + 1 else height(r) + 1 endif
  endcases measure ????
end bt
 
I cannot use the height function in the measure so how to specify this?
 
thanks for your support,
 
regards, Thijs
 


Nooit ongewenste berichten ontvangen: gebruik MSN Messenger klik hier