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

Re: PVS proofs in batch mode



Hi Cesar,
I started working on this before I saw Shankar's message.  As usual in
PVS, there are many possible solutions.  Here is an Emacs-oriented
solution, which I thought you might be interested in since you mentioned
running from a batch program.

I created a lisp function associate-proof-with-formula, and some Emacs
functions to exercise it.  You should be able to modify the Emacs
functions to suit your needs.

associate-proof-with-formula takes a theory name, a formula name (of that
theory) and a strategy, and sets the proof and writes out the .prf file.

The Emacs functions are in two separate files, so that I could generate a
theory and associate the formulas in one batch run, and then run the
proofs in a second one.  After adding the lisp function to my ~/.pvs.lisp
file, I ran these as follows:

% pvs -batch -load-after fgen.el

% pvs -batch -v 3 -load-after prove-it.el

Regards,
Sam

.pvs.lisp


fgen.el

prove-it.el