|[ << ]||[ >> ]||[Top]||[Contents]||[Index]||[ ? ]|
PVS 5.0 is a significant new release of PVS. The highlights include an SBCL port, the incorporation of the PVSio, Manip, Field, and ProofLite packages from NASA, a new theory interpretation implementation, new judgement forms, new support for Yices, and several bug fixes.
The system is installed as usual; see the download pages at
We strongly suggest getting a pre-built Allegro version, unless you have concerns with the Allegro runtime click-though license, in which case get one of the pre-built CMU or SBCL Lisp images.
Note that we are no longer providing PVS for Solaris or PowerPC on the download page, as we have limited funds and the vast majority of our users have Intel Macs or Linux machines. If you do need either of these, let us know at firstname.lastname@example.org. We will be keeping earlier versions available for the foreseeable future.
It’s important to note that the
.prf format has changed. While PVS
5.0 can easily read earlier proof files, the new format will confuse
earlier versions of PVS. Please make copies of any directories that you
want to also use earlier versions of PVS on. This is especially helpful
when trying to repair proofs that work in earlier versions.
|Manip and Field|
|PVS Libraries Speedbar|
There are now 64-bit and 32-bit versions available for Intel Mac and Linux for Allegro (version 8.2) and SBCL Common Lisp. 32-bit versions are also available for CMU Common Lisp.
pvs shell script has been modified to support SBCL Common Lisp.
In addition, the load and eval capabilities have been simplified, where
-e are for Emacs files and expressions, and
-E are for Common Lisp files. There was an earlier
flag, but it loaded the file before PVS initialization, which is
more difficult to use.
César Muñoz has provided further improvements for PVSio, which is now more fully integrated into PVS. PVSio provides
defattachmacro, allowing users to add their own semantic attachments
pvsioscript, allowing PVS specifications to be run as scripts
eval-formularules for use in the prover
PVSio now starts up without the need for loading extra library files. The
sematic attachments are pre-installed, and the supporting theories are in
the prelude. For more details on how to use PVSio, see the manual in
doc/PVSio-2.d.pdf, (but ignore the installation instructions).
The NASA Manip and Field packages have similarly been integrated, and
improved by their authors. The Manip package provides many features,
including Emacs extensions, many new proof strategies, and a pattern
matching facility that allows reference to subterms during proof. For
more details, see
doc/manip-guide.pdf (but ignore the install
The Field package builds on Manip, and adds several prover commands making
it easier to reason about nonlinear formulas. See
doc/extrategies.pdf for details.
César Muñoz has also provided his ProofLite extension as part of PVS.
This allows proofs to be included directly in PVS specifications and run
from them, allowing for a literate programming style of specification.
doc/ProofLite-4.2.pdf for details.
Theory interpretations have been significantly modified. Previously a theory declaration would generate a separate theory. This caused all kinds of problems, as it couldn’t reference any declarations from the referencing theory. In some cases this could be handled by splitting theories into pieces, but even this doesn’t always work.
In the new treatment, theory declarations are simply expanded in place,
with the theory declaration id prepended to the included theory
declarations. This solves the problem with declaration references, but
introduces new issues. First, since the expanded theory declaration may
itself have theory declarations, names have been extended to include any
number of periods, e.g.,
th1.th2.th3.d. In general, these are only
needed to disambiguate, and even then a suffix of the full name usually
prettyprint-theory-instance is no longer meaningful, simply use
M-x prettyprint-expanded to see the included declarations.
A new Judgement form is available. This is still in the experimental
stage, but we welcome any feedback. The judgement has the form of a
subtype judgement, but with a preceding
FORALL that gives the types
of the variables, as well as making the parsing unambiguous. Within the
forall, any expression is allowed. For example,
judgement forall (x: real) = x*x has_type nnreal f: [nnreal -> real] foo: formula forall (y: real): f(f((y - 100) * (y - 100)) * f((y - 100) * (y - 100))) = 2
Without the judgement,
foo generates 2 TCCs; with the judgement,
none are generated for
foo, just the one for the judgement itself,
which is much simpler to understand. Note that the judgement mechanism
has to be fast, and not itself generate proof obligations, so the matches
are purely syntactic. Thus ‘(x - 1) * (-1 + x)‘ will still generate a
There are improvements to the
rules. Note that to use these commands you must install Yices from
yices.csl.sri.com, and make certain the directory containing the
yices executable is in your
PATH environment variable before
A simple Emacs speedbar extension is now available. This makes browsing
libraries easier, as it lists all directories on the
PVS_LIBRARY_PATH as well as the built-in libraries in the
lib subdirectory. This is invoked with
pvs-speedbar-browser, and clicking on a given library shows the
specification files within; clicking on one of them brings it up in an
Emacs buffer. In the future we plan to include declaration lists within
the speedbar display.
The changes lead to some incompatibilities, primarily in the proofs. This is due to a number of factors:
lift-ifrule that could potentially lead to unsoundness. The fix means that the rule is no longer as aggressive, so proofs may need to be repaired. This is especially true for proofs with sequences of
chooseno longer has a definition, and
singletonis no longer a conversion by default. If you really want
epsilon, there is an axiom for that. The
singletonconversion is often used unexpectedly, especially when bitvectors are involved. If you want it, simply add a
conversion+ singletonwhere needed. Remember it’s imported, so it can be placed in a theory low in the hierarchy; it doesn’t have to be added to every theory. The rest of the changes are only likely to be a problem if they accidentally introduce ambiguities. These are usually easily resolved.
Most of the other incompatibilities are more obvious, and the proofs are easily repaired. If you have difficulties understanding why a proof has failed, or want help fixing it, send it to PVS bugs email@example.com.
|[ << ]||[ >> ]||[Top]||[Contents]||[Index]||[ ? ]|
This document was generated by Sam Owre on February 11, 2013 using texi2html 1.82.