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

[PVS-Help] On Individual formula proof in a batch mode

Dear members,

I tried to run PVS in a batch mode to prove each formula in a theory.
I found good help but it does not work.
The function definition is:

(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"))))

the function (status-flag) return void-function error.
If any knows why?

In addition,
I ran the following el file (pvsbatch.el) to get some stdout.
But the function (prove-formula "pvsbatch" "c1") returns the following
error message in "pvsbatch.log" file.


(let ((my-formula-result nil)
(msg (pvs-validate "pvsbatch.log" "/tmp_amd/kamen/import/1/min/Haskell/Codes/2PVS"
(let ((current-prefix-arg t))
(prove-formulas-pvs-file "pvsbatch")
(setq my-formula-result
(prove-formula "pvsbatch" "c1" t)))
(print (list 'my-prove-formula-result my-formula-result)))

>> pvsbatch.pvs:: pvsbatch: THEORY


x1, x2: VAR int

 c1: LEMMA (x1 > 0) AND (x2 > x1) IMPLIES (x2 > 0)
 c2: LEMMA (x1 > x2) AND (x1 > 0) IMPLIES (x2 > 0)

END pvsbatch

The result of pvsbatch.log is::

PVS file c1 is not in the current context
Typecheck error: Can't find file for theory c1

Great thanks for your help.