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

Re: Recursive Functions with negative domain





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
> 
>