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

*To*: pvs-help@csl.sri.com*Subject*: Re: Recursive Functions with negative domain*From*: hoffman@securecomputing.com*Date*: Wed, 21 Jul 1999 09:47:28 -0500 (CDT)*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <3795C2BE.2FB06B66@cs.uni-sb.de> from "Daniel Kroening" at Jul 21, 99 02:53:18 pm

It works just fine if you use MEASURE i+1 instead of MEASURE i John > > Hello, > > it is probably a beginner's question: > > 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: > > % Subtype TCC generated (at line 11, column 14) for i > % untried > ABC_TCC1: OBLIGATION (FORALL (i: integer | i >= -1): i >= 0); > > Despite of this TCC everything done with the function works as expected. > I tried to define an appropriate measure, but this did not change this > TCC at all. > > Thank you for your help, > > Daniel Kroening > >

**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:
**Recursive Functions with negative domain** - Prev by thread:
**Re: Recursive Functions with negative domain** - Next by thread:
**Recursive Functions with negative domain** - Index(es):