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

Re: Structural induction and local names

Scott L. Burson wrote:
> Could you show us an example?

Sure. There is a PVS dump file at
including a couple of theories and an incomplete
proof of local_names.th1.

The theories describe a world in which state
variables are attached to objects. In order to
access a state variable one first gets hold of an
object, and then looks up a function from objects
to state variables using the name (string) of the
desired field.

Running the proof results in the following sequent,
which is the induction case for universal quantification:

  {-1}  primed_value((: assign(assign1_var!1, assign2_var!1,
                               forall_q2_var!1) :),
                     s2!1, env!1)
                    (obj!1, field_name!1)
         primed_value(compose_bodies((: a1!1 :),
                                     (: assign
                                         forall_q2_var!1) :)),
                      s1!1, env!1)
                     (obj!1, field_name!1)
  [-2]  FORALL (obj2: object, field_name2: string):
          the_field_naming(field_name2)(obj2)(s2!1) =
           primed_value((: a1!1 :), s1!1, env!1)(obj2, field_name2)
  [1]   primed_value((: assign(assign1_var!1, assign2_var!1,
                                        forall_q2_var!1)) :),
                     s2!1, env!1)
                    (obj!1, field_name!1)
         primed_value(compose_bodies((: a1!1 :),
                                     (: assign
                                          forall_q2_var!1)) :)),
                      s1!1, env!1)
                     (obj!1, field_name!1)

Function primed_value uses the semantic function

   sem(e: expr_syntax, env : environment, s : state): RECURSIVE bool =
     CASES e
       OF boolconst(b): b,
          svar_ref(obj, f): the_field_naming(f)(env(obj))(s),
          and(e1, e2): sem(e1, env, s) AND sem(e2, env, s),
          forall_q(q_var, e):
            forall (ob : object):
                          env WITH [q_var := ob],
      MEASURE e BY <<

to calculate the value of state variables in the next state. The
problem arises because in {-1} the value of forall_q2_var!1 is
evaluated in environment env!1, but in [1] it is evaluated in
environment env!1 WITH [q_var := ob].

Hopefully this clarifies my question.