[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Recursive Functions with negative domain
it is probably a beginner's question:
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
(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
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,