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

*To*: pvs@csl.sri.com*Subject*: Instantiations*From*: Kellom{ki Pertti <pk@cs.tut.fi>*Date*: Mon, 5 Feb 2001 10:19:21 +0200 (EET)*Sender*: pvs-owner@csl.sri.com

Hello again, Maybe I should elaborate a bit my question about instantiation. I received a few suggestions on how to use inst? and how to do explicit manual instantiation. Hopefully the following will clarify why I am looking for a more automatic solution. I map specifications in my own specification language Ocsid to PVS in order to verify temporal properites. Let's say my specification consists of initial condition INIT and actions ACTIONS. Verifying that a formula abstract_var_implemented is an invariant yields the sequent ---------------------------------------------------------------------- abstract_var_implemented_invariance : |------- {1} invariant(abstract_var_implemented, INIT, ACTIONS) ---------------------------------------------------------------------- All variables are introduced in a syntactic construct called a layer. Layers can be used in the same way as PVS parametric theories to verify properties in an abstract form. Thus, I can use a previously verified invariant as a lemma: ---------------------------------------------------------------------- {-1} invariant(abstract_var_implemented, LAYERINIT, LAYERACTIONS) |------- [1] invariant(abstract_var_implemented, INIT, ACTIONS) ---------------------------------------------------------------------- If my compiler is correct, the lemma is guaranteed to imply the invariant I want to verify. However, I would like to do the proof within the PVS logic, so I proceed to show that LAYERACTIONS implies ACTIONS. This is where I would like a heuristics to kick in, because the sequent expands to a large number of quantified formulas (see below). It is kind of frustrating to do all the instantiation by hand, since the process is straightforward. One just has to skolemize and then instantiate variables with the corresponding Skolem constants, and the proof is practically done. As I said, this would be easy to do with e.g. HOL, so it would be nice to be able to do it in PVS as well. -- pertti ---------------------------------------------------------------------- abstract_var_implemented_invariance.3 : {-1} (Stutter(b!1(n!1), b!1(1 + n!1))) OR (EXISTS (p2_new_ax: integer, p1_new_ax: integer, p2: node, p1: node, m: message): swap(b!1(n!1), b!1(1 + n!1), p2_new_ax, p1_new_ax, p2, p1, m)) OR (EXISTS (m: message, p1: node): send_message(b!1(n!1), b!1(1 + n!1), m, p1)) OR (EXISTS (m: message, p1: node): receive_message(b!1(n!1), b!1(1 + n!1), m, p1)) |------- {1} ((swap_spec.Stutter(b!1(n!1), b!1(1 + n!1))) AND Stutter_extension(b!1(n!1), b!1(1 + n!1))) OR refined_Stutter(b!1(n!1), b!1(1 + n!1)) OR (EXISTS (p2: node, p1: node, m: message): (EXISTS (p2_new_ax: integer, p1_new_ax: integer): swap_spec.swap (b!1(n!1), b!1(1 + n!1), p2_new_ax, p1_new_ax, p2, p1)) AND communicate_extension(b!1(n!1), b!1(1 + n!1), p2, p1, m)) OR (EXISTS (m: message, p1: node): send_message(b!1(n!1), b!1(1 + n!1)) AND send_message_extension(b!1(n!1), b!1(1 + n!1), m, p1)) OR (EXISTS (m: message, p1: node): receive_message(b!1(n!1), b!1(1 + n!1)) AND receive_message_extension(b!1(n!1), b!1(1 + n!1), m, p1)) ----------------------------------------------------------------------

- Prev by Date:
**Re: Instantiation hints** - Next by Date:
**Re: Instantiation hints** - Prev by thread:
**Re: Instantiation hints** - Next by thread:
**Boolean predicate to function** - Index(es):