PVS 2.4 includes several new features and fixes a number of bugs. The system, language, and prover documents have also been updated.

The new features include

PVS arguments:
The pvs startup script allows new options. System Guide, Section 4.1:
prove-untried commands:
Commands for proving the untried formulas in the importchains and importchain subtrees have been added. System Guide, Section 3.5.2.
prove-formulas and prove-tccs commands:
These commands make it easy to apply a strategy to all the formulas or TCCs of a given theory, pvs-file, importchain, or importchain subtree. System Guide, Section 3.5.2.
Library strategy files:
Strategy files associated with libraries are now automatically loaded, allowing library developers to provide specialized strategies. System Guide, Section 3.5.4.
show-expanded-form command:
This command is like the show-expanded-sequent command, but works on a region of a specification. System Guide, Section 3.13.
New lexical operators:
Added the (|, |) and {|, |} outfix operators, which are similar to the [|, |] operators. Language Reference, Chapter 2.
Better treatment for recursive functions:
Recursive functions no longer need to be fully applied in order to check for termination. Language Reference, Section 3.4.
Well founded TCCs:
The well-founded TCC, generated when an ordering is given for a recursive function, is only generated if the relation is not declared to be well-founded. Language Reference, Section 3.4.
Macros:
This new form of definition is available. Macros are expanded during typechecking, and in some cases can make proofs more automatic. Language Reference, Section 3.5.
Conversions:
There is now better conversion control, and the K_conversion is now turned off by default. Language Reference, Section 3.9.3.
Auto-rewrite declarations:
Auto-rewrite declarations allow the sepcifier of a theory or library to specify which definitions and lemmas should always/never be used as rewrites. Language Reference, Section 3.11.
Well foundedness in datatypes:
The << relation is declared to be well-founded, rather than relying on the axiom. The axiom is retained. Language Reference, Section 8.1.
Skolem-typepreds? argument:
The skolem, measure-induct, and measure-induct+ commands now take a skolem-typepreds? argument, indicating whether to provide type predicate antecedents for the introduced Skolem constants. This makes it easier to automate certain kinds of proofs. Prover Guide, Sections 4.7.10, 4.11.5, and 4.11.6
name rule change:
The name rule now generates a definition. This allows the name to be used in expand or rewrite commands. It is also added to the auto_rewrite- table, so that commands such as grind do not expand it. Prover Guide, Section 4.8.3.
Auto-rewrite names:
In conjunction with auto-rewrite declarations, a new form of auto-rewrite name is provided, and auto-rewrite has been modified to use these (as well as the old form). See the Prover Guide, Section 4.13.1, the help-pvs-prover-command, or type (help auto-rewrite) to the Rule? prompt.
Abstraction rewritten:
See the Prover Guide, Section 4.15. The new abstractor integrates both boolean and data (scalar) abstractions. It employs various optimizations such as partitioning, and is significantly faster than the PVS 2.3 abstractor. It takes a feasible argument characterizing the concretely feasible abstract states, as needed for abstracting existential-strength quantification. The interface for the abstract command is

(abstract  cstate  astate  amap  &OPTIONAL  theories
     rewrites  exclude  (strategy ['(assert)])  feasible  verbose?).

It takes the concrete state type cstate, the abstract state type astate, and the abstraction map alist amap. The interface for the abstract-and-mc command is now

(abstract-and-mc  cstate  astate  amap  &OPTIONAL  theories
      rewrites  exclude  (strategy ['(assert)])  feasible  verbose?).

The following changes are not backward compatible. In our validation suite only a small percentage required adjustment to the specs or proofs, and those were straightforward (although it was frequently helpful to run PVS 2.3 in parallel to see the differences when repairing proofs).

TCCs are simplified:
In order to reduce the number of trivial TCCs, those that are ground are simplified, and those that reduce to true are discarded. This can lead to a renumbering of TCCs.
K_conversion is off by default:
see above.
Better term order for ground decision procedures:
The term ordering used for the ground decision procedures has been improved to take better account of non-linear terms. This leads to fewer loops, but some proofs may need adjustment.
Improved lift-if:
The lift-if command now works properly for CASES and COND expressions. This can affect existing proofs.
Trivial simplifications during substitution and replacement:
Trivial equality and boolean simplifications are now built into the substitution operations used by EXPAND, INST, etc., and the replacement operation used by REPLACE and REWRITE. This can affect existing proofs.
New quantifier simplifications:
The ASSERT command and its cousins now simplify (EXISTS x: x = 5) to TRUE, and (EXISTS x, y, z: x = y + z AND foo(x, y,z)) to (EXISTS y, z: foo(y + z, y, z)). Additionally, (EXISTS (x: T): TRUE) and (FORALL (x :T) : FALSE), for the nonempty type T, are automatically simplified to TRUE and FALSE, respectively.

The trick of introducing a dummy induction parameter as in (FORALL x: x = f(a, b, c) IMPLIES p(x)) has to be used with care since ASSERT will now simplify this to p(f(a, b, c)).

Prover Manual, Section 4.12.10.

True antecedents not simplified:
Antecedents that used to simplify to true and disappear may now be retained; this was needed in some special cases. This obviously affects the numbering of formulas in proofs.

In addition, many bugs have been fixed. Unfortunately, in order to fix all of them we would need to postpone this release even longer. The fixed bugs are marked as feedback in the PVS bugs list Also many of the examples linked to in the PVS web pages still need to be checked and upgraded to PVS 2.4.

If you have questions or suggestions, send email to pvs-bugs@csl.sri.com.

To get on the PVS mailing list, send a message to pvs-request@csl.sri.com.