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

Re: Format of the .prf files



Hi Hendrik,

Here's a summary of what is in .prf files.  I'll make sure I update the
User Guide with this information as well.  Let me know if you have any
questions about this.

Regards,
Sam

-----------

Prior to the introduction of multiple proofs in PVS 3.0, the format of
proofs was

(theory-id
 (decl-id
  script)
 ...)
...

The script had an optional '(:new-ground? t)' element consed on front, if
the new ground procedures were used.  This format is still supported for
reading (though the :new-ground? flag is ignored).  Some proof information,
such as proof status and proof time, was kept in the .pvscontext file.

For multiple proofs, the format needed to be modified, and more is kept in
the .prf file.  The format is:

(theory-id
 (decl-id
  default-proof-posn
  (id
   description
   create-date
   run-date
   script
   status
   refers-to
   real-time
   run-time
   interactive?
   decision-procedure-used)
  ...)
 ...)
...

where default-proof-posn is the (0-based) position of the default proof in
the list of proofs associated with the declaration.  The create-date is
the time that the proof was first saved, and the run-date is the time it
was last rerun.  The real-time and run-time are the time it took the last
time it was run, and interactive? indicates whether that was an
interactive run or not.  These may not really reflect the last run,
because the prove-theory, etc. commands do not write out a new .prf file.
Most of the rest of the fields should be self-explanatory.