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

[PVS-Help] Re: Tree height



Thijs,

> 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?

use the sub-term predicate << (which is generated by PVS for every
DATATYPE declaration) as follows:


 † height(T:binary_tree): recursive nat =
 † cases T of
     ...
   endcases measure T BY <<

See page 19 of the PVS language reference for an example, and pages
75f for an explanation of the predicate <<.

Kind regards,

	- Holger