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

*To*: pvs-help@csl.sri.com*Subject*: Instantiating multiple theories simultaneously*From*: Michael Hohmuth <hohmuth@inf.tu-dresden.de>*Date*: Mon, 31 Mar 2003 15:49:23 +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)

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:
**AG/EG - AX/EX in abstract-and-mc** - Next by Date:
**Re: AG/EG - AX/EX in abstract-and-mc** - Prev by thread:
**problem with transition relation (model-checking)** - Next by thread:
**AG/EG - AX/EX in abstract-and-mc** - Index(es):