Home | • | Intro | • | Wiki | • | Docs | • | FAQ | • | Download | • | Bugs | • | • | FM Tools |
---|

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:`-timeout`: In batch mode, this causes typechecking and individual proof attempts to be interrupted after the given number of seconds.`-nobg`: Normally PVS starts in the background (with the`&`control operator). This starts it in the foreground.`-raw`: This runs PVS without Emacs. This is only useful for front ends, which must do the same initialization as done by the Emacs interface.

- 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.

Home | • | Intro | • | Wiki | • | Docs | • | FAQ | • | Download | • | Bugs | • | • | FM Tools |
---|

*
Last modified: Thu 30 Nov 2006 12:15 UTC
Maintainer: Sam Owre
*