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

having problem in Recursive definition.

dear sir/madam,
	I have been trying to use a recursive definition of a function. My problem 
is that I don't understand what is MEASURE and measure function.
%%% example %%%%
decr : THEORY


r1 : VAR int
r2 : VAR nat

decr(r1,r2) : RECURSIVE int =
	(IF r2=0 THEN r1 ELSE decr(r1-1,r2-1) ENDIF)
MEASURE %%***** what measure function is to be given here *****%%

spec: THEOREM decr(r1,r2) = r1 - r2

END decr
%%% example over%%%%%
	I'd be grateful if you help me out.
	thanking you,
	yours sincerely,
	shashank shekhar.

Get Your Private, Free Email at http://www.hotmail.com