PVS 4.2 Release Notes
PVS 4.2 is primarily a bug fix release; there are few new features.
Some of the changes do affect proofs, though our experience is that
only a few proofs need adjustment, and most of these are quite easy
to recognize and fix.
Installation Notes
The system is installed as usual; see the download pages at
We strongly suggest getting a prebuilt Allegro version, unless you have
concerns with the Allegro runtime clickthough license, in which case get
the prebuilt CMU Lisp image.
Changes
 
The prelude has been modified. First, the definition of
the
has
been removed. This is to keep automatic rewrites from expanding
the
to epsilon, which is generally not useful. Proofs that used
this will need to be modified, usually by bringing in the the_lem
lemma. In addition, a number of new lemmas have been added. Here is the
complete list of changes:

From theory
sets
:
 the(p: (singleton?)): (p)
the_lem: LEMMA FORALL (p: (singleton?)): the(p) = epsilon(p)
the_prop: LEMMA FORALL (p: (singleton?)): p(the(p))
is_singleton: LEMMA
FORALL a: (nonempty?(a) AND
FORALL x, y: a(x) AND a(y) IMPLIES (x=y))
IMPLIES singleton?(a)
singleton_elt_lem: LEMMA
singleton?(a) and a(x) IMPLIES singleton_elt(a) = x
singleton_elt_def: LEMMA
singleton?(a) IMPLIES singleton_elt(a) = choose(a)
singleton_rew: LEMMA singleton_elt(singleton(x)) = x
AUTO_REWRITE+ singleton_rew


From theory
list_props
:
 every_nth: LEMMA
every(P)(l) IFF FORALL (i:below(length(l))): P(nth(l,i))


From theory
more_map_props
:
 map_nth_rw: LEMMA
FORALL (i: below(length(l))):
nth(map(f)(l), i) = f(nth(l, i))

 
César Muñoz has provided improvements for pvsio. See
doc/PVSio2.d.pdf
for details.
 
Judgements over dependent types have been fixed  in most cases this
meant the judgement was not used where it should have been, in a couple of
cases it left free variables uninstantiated, causing breaks.
 
Recursive judgements were recently introduced (see the 4.1 release notes),
and several bugs have been fixed. In addition, now when recursive
judgement has a name, the corresponding formula is generated as an axiom.
 
Autorewrites now find the proper instances; prior to this, the
autorewrites were kept in generic form, and never properly instantiated.
 
Theory interpretations have had a number of bugs fixed.
 
TCC subsumption tests have been improved, leading to fewer TCCs.
 
Batch mode now saves the context; before this, Emacs was exiting without
giving lisp a chance to save.
 
Libraries are more robust; in particular, relative library paths now work
properly when used recursively.
Incompatibilities
The changes lead to some incompatibilities. The improved judgements and
TCC subsumption lead to fewer TCCs, hence may cause TCC renumbering and
proofs may have to be shifted (Mx showorphanedproofs
may be
useful here).
In addition to these, the improved autorewrites also affect proofs, as
some branches of a proof may no longer be generated, or may have a
different form. It is usually easy to repair, though it often helps to
run an older version of PVS in parallel to figure out where the proof
deviates. Finally, any proof that relies on the expansion of the
will need to use the_lem
instead.
This document was generated by Sam Owre on February 11, 2013 using texi2html 1.82.