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

Recursive Functions with negative domain

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