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

Re: [PVS-Help] opening files and batch mode



Erika,
I don't know what kind of support for batch mode you need, but I wrote a
utility that runs pvs in batch mode, type-checks a theory, reruns all
its proofs, and produces a status report.

The utility is called proveit and is part of the ProofLite package:
http://research.nianet.org/~munoz/ProofLite

For instance if you want to rerun the proofs in test.pvs, you can type

$ proveit -clean -importchain test
Batch proving test.pvs in PVS, please be patient
Check the status of the process in ./test.out
Grand Totals: 1 proofs, 1 attempted, 1 succeeded (0.14 s)

The -clean option tells proveit to remove binary files first. The
-importchain option tells proveit to rerun all proofs in the import
chain.

Furthermore, ProofLite allows you to include proof scripts in your pvs
files, i.e.,

test : THEORY
BEGIN

  %|- *TCC* : PROOF (ASSERT) QED

  foo : LEMMA
    FORALL (x:real):
    (x+1)*(x+1) >=0
  %|- foo : PROOF (GRIND) QED

END test

After type checking, proveit will install the proof scripts in their
corresponding formulas.

I use ProofLite to automatically produce pvs files that contain
specifications and proofs. These file are then processed in batch mode.

Hope that it helps,
Cesar




On Mon, 2005-05-23 at 23:37, Erika Rice wrote:
> I want to use the batch mode of pvs and I want to open a file.  I run 
>     pvs -batch -l file.el
> where file.el contains
>     (with-open-file (str "pvs-strategies-base" :direction :input)
>       (do ((line (read-line str nil 'eof)
>                  (read-line str nil 'eof)))
>        ((eql line 'eof))
>        (format t "~A~%" line)))
> 
> However, when I run this, I get an error saying with-open-file has a
> void function definition.  
> 
> Why is this? Alternately, how can I read in a file for use in pvs
> batch mode?
> 
> Thanks,
> 
>     Erika Rice
-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace        mailto:C.A.Munoz@larc.nasa.gov
100 Exploration Way                 http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988