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

Instantiations



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))
----------------------------------------------------------------------