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

[PVS-Help] Tree height

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
  leaf (val:nat): leaf?
  node(val:nat, left:binary_tree, right:binary_tree): node?
end binary_tree
and the theory:
bt: theory
  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