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

Re: [Repost] Instantiating multiple theories simultaneously



Hi Michael,

It turns out it isn't a bug, this is part of why theory declarations were
added to the language.  The right way to do what you want is to change the
IMPORTING of A to a theory declaration, and map that at the same time you
map b:


  A : THEORY
  BEGIN
    a : int
  END A
  
  B : THEORY
  BEGIN
    Aimp: THEORY = A
    b : int
  
    ab : AXIOM a = b
  END B
  
  Aimplementation : THEORY
  BEGIN
    IMPORTING A{{a:=5}}
  END Aimplementation
  
  Bimplementation : THEORY
  BEGIN
    IMPORTING B{{Aimp := A{{a:=5}}, b:=5}}
  END Bimplementation

Note that using IMPORTING B{{Aimp := Aimplementation, b:=5}}
shoud not be allowed, because Aimplementation is not an instance
of theory A.  Some sense could be made of it in this case, but
there will be problems if it also imported A{{a:=7}}, or provided
its own declaration for a.
  
Hope this helps,
Sam

> From:    Michael Hohmuth <hohmuth@inf.tu-dresden.de>
> Subject: [Repost] Instantiating multiple theories simultaneously
> Date:    Thu, 08 May 2003 12:15:32 +0200
> To:      pvs-help@csl.sri.com
> 
> [ I am reposting this message because I did not receive a single reply
>   to my first posting.  Maybe it got lost somewhere?  --m ]
> 
> Dear PVS experts,
> 
> I have written a number of specifications, formulated in a set of PVS
> theories.  These specifications also contain a number of axioms that
> express relationships various theories' elements.  Now I want to write
> another set of theories that refine my specifications.  For this I'd
> like to use PVS' new theory instantiations.  
> 
> However, it is unclear to me how my instantiations should be
> expressed and how I best avoid all the theory-instantiation bugs that
> Hendrik Tews has recently uncovered:  See PR#'s 757--760 in
> http://pvs.csl.sri.com/cgi-bin/pvs/pvs-bug-list/pvs-bug-list?bugs=open&bugs=analyzed&originator=tews&dates=all&order=normal
> 
> Here is a simplified example of what I want to do:
> 
>   A : THEORY
>   BEGIN
>     a : int
>   END A
>   
>   B : THEORY
>   BEGIN
>     IMPORTING A
>     b : int
>   
>     ab : AXIOM a = b
>   END B
>   
>   Aimplementation : THEORY
>   BEGIN
>     IMPORTING A{{a:=5}}
>   END Aimplementation
>   
>   Bimplementation : THEORY
>   BEGIN
>     IMPORTING Aimplementation
>     IMPORTING B{{b:=5}}
>   END Bimplementation
> 
> With these specifications, PVS generates the following TCC for
> Bimplementation:
> 
>   % Mapped-axiom TCC generated (at line 23, column 14) for  B{{ b := 5 }}
>     % unfinished
>   IMP_B_ab_TCC1: OBLIGATION a = 5;
> 
> where (according to show-expanded-sequent) "a" refers to "A.a", not
> "Aimplementation.a", of course, rendering the TCC unprovable.
> 
> So my question is: How can I instantiate theories A and B
> simultaneously such that I get a TCC obligation like
> "Aimplementation.a = 5" (or "5 = 5")?
> 
> Thanks much in advance,
> Michael
> -- 
> hohmuth@sax.de, hohmuth@inf.tu-dresden.de
> http://home.pages.de/~hohmuth/