[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
Cesar A. Munoz H., Senior Staff Scientist mailto:email@example.com
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