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

Re: [PVS-Help] Regarding theory declarations



Hi Nikhil,

Theory interpretations were introduced in PVS 3.X, which allows theory
declarations to be given as formal parameters and in the body of a
theory.  Unfortunately, the obvious choice of syntax for theory
declarations was used for theory abbreviations in earlier versions of
PVS.  To fix this, simply change to the new form:

 IMPORTING theory1[Na,Pa] AS Ta
 IMPORTING theory1[Nb,Pb] AS Tb

See the release notes (M-x pvs-release-notes) for more information.

Regards,
Sam Owre


Nikhil D. Kikkeri <nikhil23@hotmail.com> wrote:

> Hi--
> 
> I have a theory
> 
> theory1[N:above(1),P:above(2)]: THEORY
> BEGIN
> 
> ......
> ......
> 
> END
> 
> what is inside the theory is not relevant for the time being. Then I have
> another theory
> 
> theory2[Na,Nb:above(1),Pa,Pb:above(2)]: THEORY
> BEGIN
> 
> IMPORTING theory1
> 
> Ta: THEORY = theory1[Na,Pa]
> Tb: THEORY = theory1[Nb,Pb]
> 
> ......
> ......
> 
> END
> 
> I am in the process of migrating certain theories from PVS 2.3 to PVS
> 3.2. While theory2 typechecks in PVS 2.3, this exact same theory does not
> typecheck in PVS 3.2
> 
> The error that I get is
> 
> "Illegal reference to Na
> May not use theory declarations with actuals or mappings that reference
> entities declared in this theory"
> 
> Is there a way to work around the problem such that the fix achieves the
> same purpose as above?
> 
> rgds
> -Nikhil
> 
> ---
> http://engr.smu.edu/~nikhil
>