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

*To*: "Cesar A. Munoz" <munoz@nianet.org>*Subject*: Re: PVS proofs in batch mode*From*: Sam Owre <owre@csl.sri.com>*Date*: Wed, 19 Nov 2003 16:01:13 -0800*cc*: pvs-help@csl.sri.com, owre@csl.sri.com*In-Reply-To*: Your message of "19 Nov 2003 14:23:05 EST." <1069269786.17725.17.camel@seahorse.nianet.org>*Sender*: pvs-help-owner@csl.sri.com

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

**References**:**PVS proofs in batch mode***From:*"Cesar A. Munoz" <munoz@nianet.org>

- Prev by Date:
**Re: PVS proofs in batch mode** - Next by Date:
**Re: PVS proofs in batch mode** - Prev by thread:
**Re: PVS proofs in batch mode** - Next by thread:
**Re: PVS proofs in batch mode** - Index(es):