[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs@csl.sri.com*Subject*: Announcing PVS Version 2.3*From*: Dave Stringer-Calvert <dave_sc@csl.sri.com>*Date*: Sat, 04 Sep 1999 18:21:08 -0700

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.

- Prev by Date:
**Suppose caml or ML had unification ....** - Next by Date:
**Proof General --- Version 3.0 release** - Prev by thread:
**Suppose caml or ML had unification ....** - Next by thread:
**Proof General --- Version 3.0 release** - Index(es):