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/.
posreal_is_nzreal: JUDGEMENT posreal SUBTYPE_OF nzrealgenerates 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.
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 nzrealor, 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?).
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 ENDIFThis 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`2whereas in the old syntax you had to rearrange things:
old syntax -> proj_2(b(a(r)))
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.
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 #)
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.
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 oldWhen 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.
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).
(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.
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.
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.
(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.
(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 - based on the
Mona tool developed at BRICS. 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.