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

Re: PVS proofs in batch mode




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