[Index]

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

http://pvs.csl.sri.com/download.shtml

We strongly suggest getting a pre-built Allegro version, unless you have concerns with the Allegro runtime click-though license, in which case get the pre-built 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/PVSio-2.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.
- Auto-rewrites now find the proper instances; prior to this, the auto-rewrites 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 (M-x show-orphaned-proofs may be useful here).

In addition to these, the improved auto-rewrites 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.

[ << ]

[ >> ]

[Top]

[Contents]

[Index]

[ ? ]

This document was generated by Sam Owre on February 11, 2013 using texi2html 1.82.