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

Re: PVS2.3 detection of theory parameters



Hi Hanne,

I believe this is a bug, I've logged it as PVS bug # 379.  I don't know
how quickly we'll be able to fix it, so for now I'm afraid you'll have to
include the nzreal parameter.

Thanks for bringing this to our attention.
Sam Owre

> From:    Hanne Gottliebsen <hago@dcs.st-and.ac.uk>
> Subject: PVS2.3 detection of theory parameters
> Date:    Tue, 16 Nov 1999 15:17:52 GMT
> To:      pvs-help@csl.sri.com
> 
> 
> 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?
> --------------------------------------------------------- 
>