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:
leaf (val:nat): leaf?
node(val:nat, left:binary_tree, right:binary_tree): node?
and the theory:
height(T:binary_tree): recursive nat =
cases T of
node(v,l,r): if height(l) > height(r) then height(l) + 1 else height(r) + 1 endif
endcases measure ????
I cannot use the height function in the measure so how to specify this?
thanks for your support,