[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*: Natarajan Shankar <shankar@csl.sri.com>*Date*: Wed, 19 Nov 2003 13:37:50 -0800*cc*: pvs-help@csl.sri.com*In-Reply-To*: Message from "Cesar A. Munoz" <munoz@nianet.org> of "19 Nov 2003 14:23:05 EST." <1069269786.17725.17.camel@seahorse.nianet.org>*Sender*: pvs-help-owner@csl.sri.com

Cesar: It is possible to write a strategy by indexing off the lemma name. Strategies can access all of the data structures. In particular, the *top-proofstate* global contains a proof state whose label field contains the id corresponding to the lemma, and the rerun strategy can be used to run a proofscript. I'm happy to write such a strategy if needed. Cheers, Shankar > From: "Cesar A. Munoz" <munoz@nianet.org> > Subject: PVS proofs in batch mode > Date: 19 Nov 2003 14:23:05 -0500 > To: pvs-help@csl.sri.com > Cc: "Cesar A. Munoz" <munoz@nianet.org> > > Hi, > > Is there a way to associate script proofs to lemmas in batch mode ? > > The long version of the question is: Assume that I have automatically > generated a PVS theory file with lemmas lem_1,...,lem_n (n is somehow > big). Assume that I know how to generate proof scripts for each one of > the lemmas, let say ps_1, ...., ps_n. Is there a quick and simple way to > associate the proofs scripts to the lemmas (ps_1 to lem_1,...,ps_n to > lem_n) by running PVS in batch mode ? > > Thanks, > Cesar

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

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