Also, there are "early-stop" versions that take an early-stop
predicate of the partial result. Before each iteration (i.e., at the
top) the HO control function tests to determine if the lo index is
less than loob and if the early-stop predicate holds of the
partial result. If either the lo index is geq the loob
or the early-stop predicate holds of the partial result, then the
partial result is returned (and the transition function is not
applied). If both the lo index is less than the loob
and the early-stop predicate does not hold, then the transition
function is applied and there is another call with the new partial
result and with the lo index increased by one.
The spec is in
nat-ho.re
SpecWeb Index | Specs |