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

*To*: pvs-help@csl.sri.com*Subject*: having problem in Recursive definition.*From*: "shashank shekhar" <shashank2000@hotmail.com>*Date*: Sat, 16 Oct 1999 12:48:14 IST*Reply-To*: shashankshekhar@mailcity.com

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 BEGIN 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. -- ******************* HAVE A NICE DAY!! ****************** ______________________________________________________ Get Your Private, Free Email at http://www.hotmail.com

- Prev by Date:
**Rewriting** - Next by Date:
**help with a question about unions (and sums)** - Prev by thread:
**help with a question about unions (and sums)** - Next by thread:
**Rewriting** - Index(es):