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