[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Announcing PVS Version 2.3
We are pleased to announce the release of PVS 2.3.
PVS 2.3 is a significant enhancement over PVS 2.2. A large effort has
been put into the optimization of several areas of the code and
experiments we have performed using a wide variety of specifications have
shown impressive speed improvements - if you have examples which show no
improvement, or worse a slowdown please send those to us at
pvs-bugs@csl.sri.com for analysis.
We tried to make this release backward compatible, but there are syntactic
changes that will require changes to the specifications, and other
changes, in particular the handling of judgements, that will require
adjustments to some proofs. In our validation suite only a small
percentage of specifications and proofs needed such adjustments, and in
every case the adjustments needed were straightforward. In some cases it
helps considerably to run a 2.2 proof side-by-side with a 2.3 proof in
order to determine the necessary changes.
The PVS documentation has been fully updated with all of the new features
of PVS 2.3. In addition, there is online documentation for some new
"experimental features" available at http://pvs.csl.sri.com/experimental/.
Installation
------------
The system is available from ftp://pvs.csl.sri.com/pub/pvs/.
The file INSTALL in that directory contains the installation instructions.
PVS 2.3 is only available for Sun computers running Solaris, and Intel
computers running Redhat Linux version 4 or higher.
What's New?
-----------
o The syntax for coercion has changed from "expr : type-expr" to
"expr :: type-expr". This change helps dramatically to reduce
the ambiguity in the grammar, and reduces the requirement for
using the separator ";".
o Judgements may be given names - the generated judgement TCC is named
after the judgement. For example:
posreal_is_nzreal: JUDGEMENT posreal SUBTYPE_OF nzreal
generates the TCC:
% Judgement subtype TCC generated (at line 1146, column 31) for x1
% proved - complete
posreal_is_nzreal: OBLIGATION FORALL (x1: posreal): x1 /= 0;
This allows you to use the generated TCC as a lemma with confidence
that the naming will be stable even if the TCCs change.
o The syntax for closure judgements has changed - using the old style
will most likely result in unprovable TCCs, as it now has different
semantics. For example, in the 2.2 syntax you could say:
JUDGEMENT * HAS_TYPE [nzreal, nzreal -> nzreal]
This is not really true - "*" doesn't have that type, but it does if
the arguments are both nzreal. In 2.3, the above implies that "*" has
that type for all arguments. The following must be used to get the
intended effect:
nzx, nzy: VAR nzreal
nzreal_times_nzreal_is_nzreal: JUDGEMENT *(nzx, nzy) HAS_TYPE nzreal
or, alternatively,
nzreal_times_nzreal_is_nzreal: JUDGEMENT
*(nzx, nzy: nzreal) HAS_TYPE nzreal
Have a look at the prelude (view with M-x vpf) for many examples of
how to use the new style of judgements, and the BNF grammar
(M-x help-pvs-bnf) for the full syntax.
The handling of judgements has been changed significantly (partly for
speed and partly to fix bugs). This can cause some proofs to fail
because the number of TCCs is a factor in the selection criteria used
by (inst?).
o There is a new alternative syntax for record accessors and tuple
projections. The old syntax is still accepted by the parser, but
all output from PVS will be in the new syntax. For example:
record : TYPE = [# b : int, c : bool #]
r : VAR record
old syntax -> IF c(r) THEN b(r) ELSE 0 ENDIF
new syntax -> IF r`c THEN r`b ELSE 0 ENDIF
tuple : TYPE = [bool,int]
t : VAR tuple
old syntax -> IF proj_1(t) THEN proj_2(t) ELSE 0 ENDIF
new syntax -> IF t`1 THEN t`2 ELSE 0 ENDIF
This syntax is also used in WITH (update) expressions. For example:
record2 : TYPE = [# a : [# b : [int,int] #], c : int #]
r : VAR record2
old syntax -> r WITH [(a)(b)(2) := 45]
new syntax -> r WITH [`a`b`2 := 45]
An advantage of this new syntax is that you can cut-and-paste the
expression from the update and it will make sense, i.e.:
new syntax -> r`a`b`2
whereas in the old syntax you had to rearrange things:
old syntax -> proj_2(b(a(r)))
o A more convenient syntax is available for LET and WHERE expressions
involving functions:
LET f: [int -> int] = LAMBDA (x: int): x * x IN f(f(x))
may instead be written as
LET f(x: int): int = x * x IN f(f(x))
Note that recursive functions may not be locally defined in this way.
o The CONTAINING clause has been moved from subtypes to type declarations.
Replace
R: TYPE+ = [# a: int, b: {x: int | x < a} CONTAINING a - 1 #]
with
R: TYPE+ = [# a: int, b: {x: int | x < a} #]
CONTAINING (# a := 1, b := 0 #)
o There are several new Emacs commands available:
o M-x help-pvs-bnf
Shows the PVS grammar
o M-x prove-next-unproved-formula
Start proof on next unproved formula
o M-x prove-theories
Do all proofs in specified theories
o M-x prove-importchain-subtree
Do proofs in specified subtree of IMPORT chain
o M-x new-decision-procedures
M-x old-decision-procedures
Use the new/old decision procedures (see later) by default
o M-x prove-theory-using-default-dp
M-x prove-theories-using-default-dp
M-x prove-pvs-file-using-default-dp
M-x prove-importchain-using-default-dp
M-x prove-importchain-subtree-using-default-dp
M-x prove-proofchain-using-default-dp
Do proofs with default decision procedures
o M-x prove-untried-pvs-file
M-x prove-untried-theory
Try running a specified strategy (e.g., (grind)) on all formulas in a
file/theory which do not yet have a proof attempted. (The command
will prompt for a theory and a strategy.)
o M-x install-and-step-proof
M-x install-and-x-step-proof
Install the current proof at formula and step
o M-x set-print-lines
Set the number of lines to print for sequent formulas
o M-x usedby-proofs
Display formulas whose proofs refer to the declaration at cursor
o M-x pvs-lisp-theory
Generate lisp file for a theory (see later)
o M-x pvs-ground-evaluator
Invoke the interactive ground evaluator (see later)
o M-x pvs-set-linelength
Set the prettyprinter line length
o M-x pvs-garbage-collect
force PVS to garbage collect (by default, just a scavenge. With
an argument forces a full gc - useful prior to demos).
o M-x report-pvs-bug
Mail a bug report to pvs-bugs@csl.sri.com
o Personal patch files: The file ~/.pvs.lisp is loaded at startup,
and whenever the command M-x load-pvs-patches is issued.
o Extended prelude: The mu calculus library is now in the prelude to
support the model checker. The finite sets definition is in the prelude
to support future extensions (ws1s decision procedure). Bruno Dutertre
was kind enough to provide the rem and divide theories. In addition,
there are a number of smaller addtions to the prelude, including a new
K_conversion theory that makes it easy to "lift" types.
o Subsumed TCCs are now included in the messages; use
M-x show-theory-messages or M-x show-pvs-file-messages to see them.
o New prover commands:
o (COMMENT string)
Attaches the comment STRING (preceded by semicolons) above the sequent.
The comment is saved in the proof, and is inherited by subgoals of the
current goal.
o (LABEL string-or-symbol fnums &optional push?)
Attaches the label STRING-OR-SYMBOL to the formulas FNUMS. The label
is printed in the sequent next to the formula number, and can
subsequently be used in any proof command in place of a formula number.
When PUSH? is T, the new label is added to any existing label - by
default it will replace any existing label.
o (WITH-LABELS rule labels &optional push?)
Executes the proof step RULE and then attaches the labels from the list
LABELS to the generated subgoals. If more subgoals are generated than
there are labels in the list, then the last label in the list is
attached to each extra goal. The PUSH? argument works as per (label).
o (FLATTEN-DISJUNCT fnums &optional depth)
An extension of the (flatten) rule. Here FNUMS is not an &rest
argument, and there is an optional :DEPTH argument which controls
the depth to which top-level disjunctions in a sequent formula are
flattened.
o Changes to existing prover commands:
o (DETUPLE-BOUNDVARS)
now works on records as well as tuples.
o (UNDO)
can now undo itself, if invoked immediately after the undo you
wish to undo.
o (BDDSIMP)
has an optional irredundant? flag which controls whether to return
redundant sequents. Defaults to T, but is quite expensive. The BDD
package has been linked as a foreign function, which makes it much
faster, especially when large terms are involved.
o (MODEL-CHECK)
now has an install-rewrites argument as per (grind), and an irredundant?
flag as in (BDDSIMP) - defaults to NIL. The model-checker package has
also been linked in as a foreign function.
o (GRIND), (REDUCE), (BASH), (USE), (INDUCT-AND-SIMPLIFY),
(MEASURE-INDUCT-AND-SIMPLIFY)
now have an extra argument :instantiator which allows you to specify
an alternative to (inst?) for the instantiation within the strategy.
o (SPLIT)
Now has a :depth argument to control the depth to which a conjunction
is split.
o (HIDE-ALL-BUT)
Reversed the arguments so that (hide-all-but (-1 2)) hides all but
formulas -1 and 2. Keep in mind that (hide-all-but -1 2) is the same as
(hide-all-but (-1) (2)) which simply hides formula 2.
o Proof checkpointing. Checkpoints may be added to the Proof buffer
(obtained by M-x edit-proof). To add a checkpoint, position the
cursor and type C-c a. The checkpoint is indicated by a double
exclamation point (!!). Any number of checkpoints may be added. When the
proof is installed using C-c C-i, these are changed to the (checkpoint)
proof rule, and branches of the proof that do not have a checkpoint on
them are wrapped in a (just-install-proof) proof rule. When this proof is
rerun, it will run until it hits a (checkpoint), and then prompt for a
prover command. When it hits a (just-install-proof), it simply installs
the given commands and marks that branch as proved. This allows the
prover to quickly get to the next checkpoint, without attempting the
proof of branches that do not have checkpoints in them. When a proof that
has (just-install-proof) rules in it is finished, the prover asks whether
the proof should be rerun, as the formula will not be considered proved
until the proof is rerun.
To remove a checkpoint from the Proof buffer, position the cursor at the
checkpoint and type C-c r. To remove all checkpoints, type C-c DEL.
The purpose of proof checkpointing is to allow you to get rapidly to
the parts of a proof you wish to examine or adjust.
o Prover input checking. The prover will now perform some basic sanity
checking on arguments to proof commands that are typed interactively,
and generate appropriate error messages when the rule is not defined,
or is given inappropriate arguments. The checking is performed on
user defined proof strategies as well as predefined ones.
o Better prover error messages are now produced. In PVS 2.2, strategies
that failed generally just printed "No change". To print out more would
be misleading when such strategies were used in other strategies that
backtrack. The strategy could be rerun in its expanded ('$') form to
find out the problem. Now messages are stacked, and when a strategy
ends with no change, the first and last messages produced during the
execution of the strategy are printed.
o New decision procedures. By default, you will use the same decision
procedures as in PVS 2.2 (due to Rob Shostak). In PVS 2.3, you also have
the choice of using our new decision procedures (implemented by David
Cyrluk). Presently they decide a little more than the old decision
procedures, but are being used as a base to significantly extend the
number of decided theories.
To change the default decision procedures use M-x new-decision-procedures
and M-x old-decision-procedures. PVS will prompt you at the start of
a proof if the proof was developed with decision procedures that are
not the current default. You can also force PVS to use a particular set
of decision procedures for the current session by a command line
argument:
pvs -force-decision-procedures new
pvs -force-decision-procedures old
When the decision procedures are "forced" like this, the default as set
with the above emacs commands has no effect.
The new decision procedures try to reproduce the behavior of the old
decision procedures. Occasionally they will cause some proof branch to
finish earlier, and the proof may then get out of step, causing the
overall proof to fail. You will need to adjust the proof in these rare
cases.
o New Prettyprinter. A completely new prettyprinter (both text and LaTeX)
has been implemented, which is much faster than the previous Ergo
generated one. If you find examples of expressions which you think
could be be more effectively prettyprinted, please send the expression
to us at pvs-bugs@csl.sri.com (you don't need to send all the files -
just the particular string that doesn't print nicely).
The new prettyprinter is sensitive to the line length, which used to be
determined whenever the window was resized, but is now set to the
startup window size. To reset it, use M-x pvs-set-linelength.
The display of sequents during proof may be controlled by using
(set-print-depth), (set-print-length), and/or (set-print-lines). The
depth indicates the amount of nesting, length the length of arguments,
and lines the number of lines printed before elision. Print-lines is per
formula in the sequent, thus if you set-print-lines to 5, each formula
in the sequent will print only the first 5 lines. These commands are
both Emacs commands and proof commands that otherwise act as a (SKIP).
o Emacs interface updated. The Emacs <-> Allegro interface has been
updated to the latest ILISP code, and the entire emacs code has been byte
compiled for extra performance and lower startup time. There is no
longer any support for Emacs 18, but the support for GNU Emacs 20,
XEmacs 20 and XEmacs 21 is much improved.
o Incorporation of "experimental features" - these are features which will
be in PVS 3.0, but are provided in PVS 2.3 for
experimentation and feedback. The interfaces to them are not
guaranteed to remain the same in PVS 3.0 and the code is still being
actively worked on, so feedback/wishlists/etc. will be appreciated (as
it is for all features of PVS). A brief overview of these features is
provided below. More detailed documentation is available on the web at
http://pvs.csl.sri.com/experimental/.
o Better instantiation
(INST! &optional fnums subst where copy? if-match complete?
relativize verbose?)
Like (INST?)this strategy extends the capabilities of the INST rule,
but it tries to be more careful than (INST?) in selecting candidate
instantiations.
(INST!) simultaneously searches for instantiations for the top-level,
existential strength variables of all of the FNUMS formulas. Hereby,
it restricts its search to the formulas in WHERE. First, a full case
split for the formulas specified by FNUMS and WHERE is computed; e.g.
a formula in the hypothesis of the form "(EXISTS (x: { y: T | P(y)}):
Q(x) => R(x))" gives rise to three sequents in the split corresponding
the the two parts of the implication and the predicate subtype. If the
RELATIVIZE? flag is unset, however, then predicate subtypes are being
ignored in the split. In the next step, a sequence of instantiations
is generated by unifying complementary pairs in the sequents of the
case splits.
If such an instantiation can not be found then the current proof
sequent is left unchanged. If there are several possible complete
set of instantiations then INST! chooses a heuristically best one if
the IF-MATCH flag is set to BEST. This is done by giving a score to
each candidate instantiation, which measures the prospect of
continuing the proof construction. The score roughly corresponds to
the number of sequents in the full case split of the current proof
sequent for which one can find complementary atoms after applying the
instantiation.
o Ground evaluation (eval), M-x pvs-ground-evaluator
PVS can now evaluate ground expressions, by translating definitions
into lisp code, which is then compiled and executed. This can be
used to "run" a specification as if were a program, many times faster
than can be achieved using rewriting. Static analysis for live
variables allows safe use of destructive updates so that compiled
PVS runs at speeds comparable to an imperative program.
There is a read-eval-print loop available by typing
M-x pvs-ground-evaluator which will put you into the *pvs* buffer and
prompt for input (PVS expressions, enclosed in double quotes). Type
help to the prompt for commands available.
A rule is available in the prover (eval) which will evaluate a given
ground expression in the context of the current proof goal. It
currently has no effect in the proof other than to print the result
of evaluation, but in future releases of PVS will be available to
perform simplification by evaluation.
o quantifier elimination (qe)
Attempts to replace formulas by equivalent, quantifier-free formulas
if such a form can be constructed. Currently supports elimination of
quantifiers over the Booleans, integers, rationals, reals and
predicate subtypes thereof, by use of the decision procedures and
Fourier-Motzkin elimination.
o Boolean Abstraction (abstract)
(ABSTRACT list-state-predicates &optional cases-rewrite?[T]
exclusive? proof-counter)
An abstract compiler for PVS assertions based on boolean abstractions.
First rewrites temporal operators into mu/nu expressions, performs
abstraction based on the list of state predicates, and simplifies.
See http://pvs.csl.sri.com/experimental/abstract.html for details, and
a link to a CAV paper describing the implementation.
o Decision procedure for WS1S
(WS1S &optional fnums examples?[t] automaton? traces? verbose?[t]
defs[!] theories rewrites exclude)
A decision procedure for WS1S - the weak second-order monadic logic
of one successor. The WS1S strategy rewrites the formulas specified by
FNUMS, and the resulting formulas are then translated, using the rule
(WS1S-SIMP), to an automaton which recognizes the language of their
interpretations. Subformulas that do not appear to be in the WS1S
fragment are abstracted away by introducing new parameters. If the final
automaton recognizes the full set, the FNUMS formulas are replaced by
TRUE; otherwise, these formulas are left unchanged.
The DEFS, THEORIES, REWRITES, and EXCLUDE arguments are used to install
rewrites. For a precise description of their meaning see
e.g. (AUTO-REWRITE-THEORY) or (INSTALL-REWRITES).
In case where the formulae specified by FNUMS are neither valid nor
unsatisfiable both a witness and a counterexample are displayed if the
flag EXAMPLES? is set. Expressions are displayed for both the free
variables in the FNUMS formulas and the newly introduced abstraction
parameters. An alternative, trace-oriented view of the examples are
displayed if the TRACES? flag is on. With the AUTOMATON? flag turned on,
the constructed automaton is displayed.
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.
We hope you find PVS useful and fun,
The PVS Team.