[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Recursive Functions with negative domain
Daniel,
> I'd like to define a function with its domain containing negative
> numbers, such as:
>
> ABC(i:integer | i>=-1): RECURSIVE integer =
> IF i=-1 THEN
> 0
> ELSE
> ABC(i-1)
> ENDIF
> MEASURE i
>
> 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.
The MEASURE function must map the arguments of the recursive functions to 'nat' (or
'ordinal'). Use MEASURE i+1 and the TCC will turn into
% Subtype TCC generated (at line 11, column 14) for i
% untried
ABC_TCC1: OBLIGATION (FORALL (i: integer | i >= -1): i + 1 >= 0);
Cheers,
- Holger
--
----------------------------------------------------------------------
Holger Pfeifer Tel.: (+49) 731 / 502-4124
Universitaet Ulm Fax: (+49) 731 / 502-4119
Abt. Kuenstliche Intelligenz pfeifer@ki.informatik.uni-ulm.de
D-89069 Ulm http://www.informatik.uni-ulm.de/ki/pfeifer.html
----------------------------------------------------------------------