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

PVS2.3 detection of theory parameters




Having moved from PVS2.2 to 2.3 I have a problem concerning using
parameterised theories.


Using PVS2.2 the following two lemmas both typechecked correctly.
"continuous" is defined in a parameterised theory, and the parameter is
the domain of the function (here nzreal).

n0x, n0y : VAR nzreal

test5 : LEMMA
  continuous(LAMBDA n0x : 1/n0x, n0y)

test12 : LEMMA
  continuous(LAMBDA n0x : 1 / n0x, 1)

However, using 2.3 test12 generates a TCC :

test12_TCC1: OBLIGATION FORALL (x: real): x /= 0;

But this works fine:

test12 : LEMMA
  continuous[nzreal](LAMBDA n0x : 1 / n0x, 1)

test5 works with both versions of PVS.

It seems like PVS (now) takes the most general of the relevant types
around and use that, unless the parameter is specified. 

Is this the case?
And is it intentional?
And is there anything I can do about it? (apart from giving the
parameter).


Thanks,
Hanne Gottliebsen
---------------------------------------------------------
Hanne Gottliebsen		    Office P337
Dept. of Computer Science	    Ph: +44 1334 46 3265
University of St Andrews	    hago@dcs.st-and.ac.uk
                   - Who moved the stone?
---------------------------------------------------------