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

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

Or alternatively, you can download ProofLite (http://research.nianet.org/~munoz/ProofLite ), which, among other things, provide the command line utility "proveit" that invokes PVS in batch mode and reproves a set of PVS theories.


On Sep 4, 2008, at 2:43 AM, Sam Owre wrote:

Hi Min,

When there is no error, prove-formula returns a proof tree, and
status-flag returns a slot of that.  But when things go wrong
(formula not found, etc.), it returns nil.  So your code should
be more like:

(defun my-prove-formula (theoryname formname)
 (let* ((*suppress-printing* t)
	 (*printproofstate* nil)
	 (*proving-tcc* t)
	 (prooftree (prove-formula theoryname formname t)))
   (if (and prooftree (eq (status-flag prooftree) '!))
       (format t "~%Formula proved")
	(format t "~%Formula unproved"))))

However, this does not explain why you get a void-function
error - you should be getting a "no methods applicable" error
if status-flag is applied to something other than a
proof tree. Are you using your own package?  If so, you may
need to invoke 'pvs::status-flag', or import the PVS package.
If this doesn't explain it, let me know.

As for batch, prove-formula is really for interactive use, and
doesn't work well in batch mode.  For PVS validations I use
pvs-validate-typecheck-and-prove My batch file for what you're
trying to do would look something like:

(pvs-validate "pvsbatch.log"
(pvs-validate-typecheck-and-prove "pvsbatch" nil nil "pvsbatch" "c1"))

The arguments to pvs-validate-typecheck-and-prove are:

(filename &optional show-proofp importchainp theory formula)

Where: filename is the pvs filename (without the .pvs extension)
      show-proofp is t to show the proof details
      importchainp is t to prove all formulas of the importchain
      theory is the theory name (recall that a single pvs file
             may have many theories)
      formula is the name of the formula to be proved
If formula and/or theory are given, importchainp must be nil.
If formula is not given, then all formulas of the
  theory/pvsfile/importchain  are attempted.

Hope this helps,
Sam Owre
Kyongho Min <min@xxxxxxxxxxxxxxx> wrote:

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"
              (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: 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.



Cesar Munoz (NIA) munoz@xxxxxxxxxx