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