Sometimes you want to know how many proof steps a particular proof takes, or how often you've used a particular proof command. This can be interesting when you are evaluating a new strategy (say, how much typing does manip save in a given proof?). Proof statistics for PVS are somewhat difficult to come by, as far as I can see -- after running a proof, PVS will tell you the time it took, and with M-x show-proof you can examine the proof directly, but that's no way to come up with quick stats for 90 invariant proofs.

Enter LISP. It's easy to read in proof files and manipulate the symbolic structures in them, so we can use a simple LISP tool to produce output like the following:

INDUCT                   1
SKOLEM                   1
BETA                     1
ASSUMING-TCC             1
NAME                     2
INST?                    5
IFF                      5
REVEAL                  11
HIDE                    12
GRIND                   15
SKOLEM!                 26
COMMENT                 40
INST                    44
LEMMA                   46
GROUND                  58
REPLACE                 79
CASE                    80
LIFT-IF                 91
PROPAX                 103
DELETE                 114
USE                    196
SPLIT                  198
EXPAND                 578
FLATTEN                615
ASSERT                 933

What does this tell us? For one thing, hitting tab-a tab-f after nearly every proof step is a lousy habit to get into. Secondly, nearly none of the advanced proof strategies available in PVS are being used. After adapting the proofs somewhat to remove superfluous (assert) and using (grind) where possible, we have a considerably smaller proof of, say, three proof commands per theorem. Such a proof is easier to maintain and quicker to re-run for verification if the underlying theory changes.

All in all this tool is useful for roughly judging how much effort is put into a particular proof, but of course there is no real metric involved and I would suggest against saying things like "40 steps is better than 45," although 5 is indubitably better than 158, which is my greatest improvement so far from hand-proved to finely-tuned (grind).

Installation: You will need a LISP system available to run these proofs. Emacs and Allegro come to mind, since you already have those available for PVS' use. I haven't tried them, I use CMU Common Lisp (CMUCL) instead since that is available as a separate command-line tool. Once LISP is installed (portinstall cmucl for some), it can be invoked and told to read the showproof.list file:

$ lisp -load showproof.lisp

Usage: The most typical use of this package is to produce statistics for all the proofs belonging to a particular PVS file (usually synonymous with the theory contained in it). The invocation for this is:

* (show-proof-file "filename.prf")

You can list multiple files for comulative totals as well, though you will need to quote the list of files as follows:

* (show-proof-file '("filename.prf" "otherfile.prf"))

Sometimes you want the statistics on only one (or a few) of the proofs in the proof file. To do this, set the global variable *pvs-proof-names* to a list of symbols corresponding to the lemma names, ie.

* (setq *pvs-proof-names*  '(|Ga1|))

if you are only interested in the proof of lemma Ga1 (the mapping of lemma names to proof names can be tricky; either peek at the .prf file or let the statistics tool list the lemma names for you.

Getting additional output: There are hooks for printing out the files, proofs, and proof-steps as they are processed. These hooks are (print-step-name*) (print-lemma-name*) and (print-theory-name*). By default, only theory names are printed, but you can redefine the functions as you see fit, for instance:

(defun print-lemma-name* (name)
  ( t "Lemma ~S~%" name))

This will print out the names of lemmas as they are processed, in the same as you should enter them in *pvs-proof-names*.

Last changed Mon Nov 1 15:46:35 MET 2004