[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
Singapore