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

*To*: Pu Zhang <zhangpu@cas.mcmaster.ca>*Subject*: Re: PVS batch mode*From*: Dave Stringer-Calvert <dave_sc@csl.sri.com>*Date*: Tue, 03 Apr 2001 15:30:31 -0700*cc*: pvs-help@csl.sri.com*In-Reply-To*: Message from Pu Zhang <zhangpu@cas.mcmaster.ca> of "Tue, 27 Mar 2001 15:07:31 EST." <3AC0F303.505EBA92@cas.mcmaster.ca>*Sender*: pvs-help-owner@csl.sri.com

> To my understanding, PVS batch mode can automatically reprove the > theorems that have already been proved manually (i.e. with interaction), > but it cannot automatically prove new theorems that have never been > proved, right ? The PVS batch mode can do nearly anything that can be accomplished in interactive mode - i.e. anything you can reduce to a sequence of emacs or Lisp commands. > I've generated hundreds of theorems using C/C++, and I want to use PVS > to prove them automatically (i.e. not first prove them with interaction > , and then rerun the proof). How can I pass the theorems to PVS and > have them proved? I've read chapter 5 in the manual, but haven't found > the answers. There's a short piece of Emacs lisp below. Put this in the file "prove-all.el" in the current directory, and replace "test" with the name of a PVS file that contains unproven theorems. Then run: pvs -q -batch -v 3 -l prove-all.el and it will attempt (grind) on each unproven theorem and TCC. I've also included an example PVS file and example output from the batch processing. Dave -------------<prove-all.el>-------------------------------- (pvs-message "Proving all unproven theorems in test.pvs") (typecheck "test") (let ((current-prefix-arg t)) (prove-untried-pvs-file "test" "(grind)")) (pvs-message "Completed") ------------<test.pvs>------------------------------------- test: THEORY BEGIN a : theorem 1 < 2 b : theorem 2 < 3 c : theorem 3 < 4 d : theorem 4 < 5 END test ------------<example output>------------------------------- Loading pvs-load... Started initializing ILISP Finished initializing pvsallegro Loading compiled patch file /project/pvs/pvs2.3/patch2.lfasl Context changed to /tmp/p/ Proving all theorems in test.pvs Parsing test test parsed in 0.00 seconds Typechecking test test typechecked in 0.01s: No TCCs generated Proving untried formula a a : |------- {1} 1 < 2 Rerunning step: (GRIND) Trying repeated skolemization, instantiation, and if-lifting, Q.E.D. Proving untried formula b b : |------- {1} 2 < 3 Rerunning step: (GRIND) Trying repeated skolemization, instantiation, and if-lifting, Q.E.D. Proving untried formula c c : |------- {1} 3 < 4 Rerunning step: (GRIND) Trying repeated skolemization, instantiation, and if-lifting, Q.E.D. Proving untried formula d d : |------- {1} 4 < 5 Rerunning step: (GRIND) Trying repeated skolemization, instantiation, and if-lifting, Q.E.D. Proof summary for theory test a...........................................proved - complete [O](0.07 s) b...........................................proved - complete [O](0.01 s) c...........................................proved - complete [O](0.02 s) d...........................................proved - complete [O](0.01 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.11 s) Grand Totals: 4 proofs, 4 attempted, 4 succeeded (0.11 s) Completed

**References**:**PVS batch mode***From:*Pu Zhang <zhangpu@cas.mcmaster.ca>

- Prev by Date:
**Re: Record-type equality bug??** - Next by Date:
**formalizing integration** - Prev by thread:
**PVS batch mode** - Next by thread:
**How understanding better pvs through some examples?** - Index(es):