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