[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS] Survey on NASA PVS Library use
On Friday 10 September 2004 14:59, Ricky W. Butler wrote:
> Dear PVS user:
> We would like to make several improvements in the naming
> schemes being used in the NASA libraries, and would like to
> get some idea of the potential impact of library changes on
> the user community. We would also like to gain some feedback
On the subject of name-changes, a rename-definition command (or heck,
rename-lemma to keep it a little simpler) would be very useful during theory
development, when you decide that defrobnicate_woodchucks: is a silly name
for an essential lemma and you want to rename it and _don't_ want the pain of
having to search-and-replace in every proof that uses the lemma.
> 4. What additional libraries or strategies would be useful to you?
Some (awfully simple) strategies I use are:
When doing (split) on an implication, A -> B, don't lose the A.
Repeared lift-if and split and simplify for CASES.
These aren't very exciting, but they save me a few steps here and there.
Analysis of proofs that I do turn up histograms like the following (this is
from a proof file dealing with verification of a protocol):
There's a couple of home-grown strategies in there, and only about 20
different real PVS prover commands, most of them "simple". I find I don't
need -- or rather, don't _use_ -- the more complicated strategies for one
simple reason: when they don't work, I'm going to need to do the "machine
language" proof hacking _anyway_ to solve the problem, so it's faster for me
most of the time to just do the manual work of a "machine language" proof
than to look up which of the hundred-odd PVS rules or strategies might fit
the current sequent best.
In that sense, _fewer_ strategies would be a nice thing to have, or perhaps
some other documentation form for the existing strategies than an
alphabetical list. When one concentrates on a single field of application of
PVS and a single framework, then it makes sense to have a richer vocabulary
in order to shorten proofs ("Induction on the structure of M" is one of my
favorite kinds of proofs when the context is well established).
One of the really nice things about manip is its means to specify formulas and
subformulas. Having long constant strings based on a specific sequent form
(say, in an (inst) command) makes PVS proofs somewhat brittle, and it'd be
nice to have something more flexible, like
(inst -1 ('re 2 "Foo(.*)"))
(which could mean "Match formula 2 against the RE Foo(.*) while keeping parens
balanced and use that to (inst) in formula -1").
As of September 1st, 2004, the University of Nijmegen will _still_ be the
University of Nijmegen, but with a different nonsensical adjective in front.
Reach me at email@example.com instead. GPG FEA2 A3FE