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

*To*: pvs-help@csl.sri.com*Subject*: [Repost] Instantiating multiple theories simultaneously*From*: Michael Hohmuth <hohmuth@inf.tu-dresden.de>*Date*: Thu, 08 May 2003 12:15:32 +0200*Sender*: pvs-help-owner@csl.sri.com*User-Agent*: Gnus/5.090012 (Oort Gnus v0.12) XEmacs/21.4 (Common Lisp,i386-debian-linux)

[ 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: strange problem with EG operator (fwd)** - Next by Date:
**Re: [Repost] Instantiating multiple theories simultaneously** - Prev by thread:
**Re: id resolution** - Next by thread:
**Re: [Repost] Instantiating multiple theories simultaneously** - Index(es):