Re: [Repost] Instantiating multiple theories simultaneously

[Sam Owre <owre@csl.sri.com>]

Michael,

This is a bug, the TCC should be as you suggest.
I'm looking into it now.

Regards,
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/