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

Re: pvs question/suggestion...



Paul Kolano has asked a number of good questions lately.  Here are
some partial answers.

> One thing I've noticed is that some of the TCCs that are not finished
> off by the tcc strategy could have been if it only had access to a few
> rewrite rules of the encoding.

Each of the TCC strategies (SUBTYPE-TCC, TERMINATION-TCC, EXISTENCE-TCC,
ASSUMING-TCC, CASES-TCC, WELL-FOUNDED-TCC, SAME-NAME-TCC,
COND-DISJOINT-TCC, COND-COVERAGE-TCC) is defined as some variation
of the strategy TCC, which in turn is defined as (grind$ :defs defs).

The way to change a tcc strategy is to redefine it in your
pvs-strategies file.  For the effect Paul wants, we'd suggest
defining it using GRIND and supplying the REWRITES and THEORIES
arguments.

> ... I will have a theory that just consists of a bunch of
> theorems that are not necessarily true and want to use a single
> command to attempt the proofs of all of them using the same predefined
> strategy.

If we understand you correctly, you want a variant of M-x tcp
that automatically applies a single proof strategy to each formula
in a theory and quits the proof if the strategy fails to prove the
formula.  This can be done, but we (Sam) would have to write it.  

> ...so what I'd like to know is whether there's any way to use one subgoal
> as a lemma in the proof of another subgoal (other than going back to
> the spec and explicity writing a lemma, that is).

There is a command M-x add-declaration that lets you augment a PVS
specification on the fly (there's also a M-x modify-declaration that
lets you change an existing declaration).  When you discover a subgoal
that looks like it embodies a lemma that ought to be generally useful,
type M-x add-decl at the point in the spec where you'd like the lemma
to appear (in order for it to be visible in the current proof, the
cursor obviously needs to somewhere above the formula you're proving),
formulate the lemma in the buffer that comes up (cutting and pasting
formulas from the subgoal), terminate with C-c C-c, and continue your
proof (presumably citing the lemma).  PVS lets you you complete the
proof, but notes that the specification was modified mid-proof and
asks if you'd like to rerun the proof "clean" to check that it replays
correctly.  This is mainly a concern with modify-declaration because
an obsolete version of the declaration might have been used in some
early parts of the proof.  Proofs may fail to rerun after add-declaration
because proof commands like auto-rewrite-theory on the current theory
might cause different behavior with and without the declaration.

To find out whether a particular formula would be useful as a lemma,
you can use the command (case "...type the formula here..") and see if
that helps you finish the proof; abandon the proof when it starts on
the branch that entails proving the formula and modify the
specification to include the formula if it was, indeed useful.

Please ask again if you need more information,
John, Sam, Shankar
-------