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

*To*: Michael Hohmuth <hohmuth@inf.tu-dresden.de>*Subject*: Re: [Repost] Instantiating multiple theories simultaneously*From*: Sam Owre <owre@csl.sri.com>*Date*: Thu, 08 May 2003 16:13:20 -0700*cc*: pvs-help@csl.sri.com, owre@csl.sri.com*In-Reply-To*: Your message of "Thu, 08 May 2003 12:15:32 +0200." <7s4r45n3qz.fsf@agnes.inf.tu-dresden.de>*Sender*: pvs-help-owner@csl.sri.com

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/

- Prev by Date:
**Re: [Repost] Instantiating multiple theories simultaneously** - Next by Date:
**about the tuple type** - Prev by thread:
**Re: [Repost] Instantiating multiple theories simultaneously** - Next by thread:
**Re: strange problem with EG operator (fwd)** - Index(es):