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

SPLIT*                   1
EXISTENCE-TCC            1
BETA                     1
INDUCT                   2
SKOLEM                   2
NAME                     2
TYPEPRED                 3
ASSUMING-TCC             3
INST?                    5
IFF                      5
SUBTYPE-TCC              9
HIDE                    15
AUTO-START              23
REVEAL                  30
AUTO-STEP               31
GRIND                   32
COMMENT                 40
SKOLEM!                 40
LEMMA                   61
INST                    64
GROUND                  88
CASE                    89
LIFT-IF                106
PROPAX                 111
REPLACE                113
DELETE                 145
SPLIT                  208
USE                    258
EXPAND                 644
FLATTEN                669
ASSERT                1107

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 groot@kde.org instead. GPG FEA2 A3FE