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

*To*: pvs-help@csl.sri.com*Subject*: Recursive Functions with negative domain*From*: "Paul S. Miner" <p.s.miner@larc.nasa.gov>*Date*: Wed, 21 Jul 1999 10:49:58 -0400 (EDT)*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <3795C2BE.2FB06B66@cs.uni-sb.de>*References*: <3795C2BE.2FB06B66@cs.uni-sb.de>

Daniel Kroening writes: > I'd like to define a function with its domain containing negative > numbers, such as: > > > testtheorem: THEORY > > BEGIN > > ABC(i:integer | i>=-1): RECURSIVE integer = > IF i=-1 THEN > 0 > ELSE > ABC(i-1) > ENDIF > MEASURE i > > END testtheorem > > (not really reasonable) > > The problem is that PVS generates a TCC, which can't be proven: Daniel, The simplest solution to your problem is to coerce your measure into the natural numbers. ABC(i:integer | i>=-1): RECURSIVE integer = IF i=-1 THEN 0 ELSE ABC(i-1) ENDIF MEASURE i+1 In this case, PVS easily discharges the generated TCC. Alternatively, you may define a well founded measure on the type upfrom(-1). ABC(i:upfrom(-1)): RECURSIVE integer = IF i=-1 THEN 0 ELSE ABC(i-1) ENDIF MEASURE i by (lambda (i,j:upfrom(-1)): i < j) Here, PVS generates a TCC asking you to prove that (lambda (i,j:upfrom(-1)): i < j) is well founded. This can be proven with a little effort using the axiom wf_nat from the prelude. (The proof is left as an exercise). Regards, -- -- Paul S. Miner | phone: (757) 864-6201 -- 1 South Wright St. / MS 130 | fax: (757) 864-4234 -- NASA Langley Research Center | mailto:p.s.miner@larc.nasa.gov -- Hampton, Virginia 23681-2199 | http://shemesh.larc.nasa.gov/~psm/

**References**:**Recursive Functions with negative domain***From:*Daniel Kroening <kroening@cs.uni-sb.de>

- Prev by Date:
**Re: Recursive Functions with negative domain** - Next by Date:
**Help - using PVS** - Prev by thread:
**Re: Recursive Functions with negative domain** - Next by thread:
**even & odd** - Index(es):