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

[PVS-Help] proving indicated formula in batch mode

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