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

Re: [PVS-Help] proving indicated formula in batch mode

I have written a PVS package to prove formulas and theories in batch
mode. See http://research.nianet.org/~munoz/ProofLite.

Hope that it helps,


On Fri, 2007-02-02 at 05:36, Yuan Ling wrote:
> Hi list members,
>      We are now mechanically verifying the fault tolerant properties of safety critical distributed systems. 
> We want to prove a formula of a theory in batch mode, because the proof strategy for this formula has already
> been generated. However, I haven’t found any suitable command in the PVS system guide for this. After viewing the help site of PVS, I found that Mr. Sam Owre has defined a function for this, which is shown below:
> (defun my-prove-formula (theoryname formname)
>   (let ((*suppress-printing* t)
>         (*printproofstate* nil)
>         (*proving-tcc* t))
>     (if (eq (status-flag (prove-formula theoryname formname t)) '!)
>         (format t "~%Formula proved")
>         (format t "~%Formula unproved"))))
> My problem is that how I can use this function as a PVS system command in batch mode? For example, I can write 
> (my-prove-formula (theoryname forname) “apply then* (flatten) ……(assert)”) in the .el file?
> Thank you very much!
> Best Regards
> Yuan Ling
> School of Computing, NUS
> Singapore
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, Room 214       http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4