[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*: Daniel Kroening <kroening@cs.uni-sb.de>*Date*: Wed, 21 Jul 1999 14:53:18 +0200*Organization*: University of Saarland, Dept. of Computer Science*Sender*: kroening@cs.uni-sb.de

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

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