Introduction

PVS 3.0 beta is now available. We are still working on updating the documentation, integration of the ICS decision procedures, and completing the validation tests, but we wanted to make it available so that others may try out some of the new features and provide feedback into the next release. Please let us know of any bugs or suggestions you have by sending them to pvs-bugs@csl.sri.com

You can download it here.

In addition to the usual bug fixes, there are quite a few changes to this release. Most of these changes are backward compatible, but the new multiple proofs feature makes it difficult to run PVS 3.0 in a given context and then revert back to an earlier version. For this reason we strongly suggest that you copy existing directories (especially the proof files) before running PVS 3.0 on existing specifications.

With the exception of commercial entities, if you have an existing license for PVS, you may upgrade to PVS 3.0 without signing a new license. For information on commercial licenses for PVS 3.0, please contact pvs-licensing@csl.sri.com

Allegro 6.0 Port

PVS 3.0 has been ported to the case-sensitive version of Allegro version 6.0. This was done in order to be able to use the XML support provided by Allegro 6.0. We plan to both write and read XML abstract syntax for PVS, which should make it easier to interact with other systems.

Theory Interpretations

Theory interpretations are described fully in Theory Interpretations in PVS

NOTES:

Multiple proofs

PVS now supports multiple proofs for a given formula. When a proof attempt is completed, either by quitting or successfully completing the proof, the proof is checked for changes. If any changes have occurred, the user is queried about whether to save the proof, and whether to overwrite the current proof or to create a new proof. If a new proof is created, the user is prompted for a proof identifier and description.

In addition to a proof identifier, description, and proof script, the proof objects contain the status, the date of creation, the date last run, and the run time.

Every formula that has proofs has a default proof, which is used for most of the existing commands, such as prove, prove-theory, and status-proofchain. Whenever a proof is saved, it automatically becomes the default.

Three new Emacs commands allow for browsing and manipulating multiple proofs: display-proofs-formula, display-proofs-theory, and display-proofs-pvs-file. These commands all pop up buffers with a table of proofs. The default proof is marked with a `+'. Within such buffers, the following keys have the following effects.

Key Effect
c Change description: add or change the description for the proof
d Default proof: set the default to the specified proof
e Edit proof: bring up a Proof buffer for the specified proof; the proof may then be applied to other formulas
p Prove: rerun the specified proof (makes it the default)
q Quit: exit the Proof buffer
r Rename proof: rename the specified proof
s Show proof: Show the specified proof in a Proof: \bkt{id} buffer
DEL Delete proof: delete the specified proof from the formula

Library relative pathnames

The system now is careful to use relative pathnames instead of absolute pathnames whenever possible in saving information in the .pvscontext and .bin files. The only reason this wasn't done in the past is that the situation in which a theory refers to a library with a relative pathname, which in turn refers to a library with a relative pathname was difficult to resolve correctly.

Cotuple types

PVS now supports cotuple types (also known as coproduct or sum types) directly. The syntax is similar to that for tuple types, but with the `,' replaced with a `+'. For example,

   cT: TYPE = [int + bool + [int -> int]]

Associated with a cotuple type are injections IN_i, predicates IN?_i, and extractions OUT_i (none of these is case-sensitive). For example, in this case we have

   IN_1:  [int -> cT]
   IN?_1: [cT -> bool]
   OUT_1: [(IN?_1) -> int]

Thus IN_2(true) creates a cT element, and an arbitrary cT element c is processed using CASES, e.g.,

   CASES c OF
     IN_1(i): i + 1,
     IN_2(b): IF b THEN 1 ELSE 0 ENDIF,
     IN_3(f): f(0)
   ENDCASES

This is very similar to using the union datatype defined in the prelude, but allows for any number of arguments, and doesn't generate a datatype theory.

Typechecking expressions such as IN_1(3) requires that the context be known. This is similar to the problem of a stand alone PROJ_1, and both are now supported:

    F: [cT -> bool]
    FF: FORMULA F(IN_1(3))
    G: [[int -> [int, bool, [int -> int]]] -> bool]
    GG: FORMULA G(PROJ_1)
	 
This means it is easy to write terms that are ambiguous:
    H1: FORMULA IN_1(3) = IN_1(4)
    H2: FORMULA PROJ_1 = PROJ_1
	 
This can be disambiguated by providing the type explicitly:
    H1: FORMULA IN_1[cT](3) = IN_1(4)
    H2: FORMULA PROJ_1 = PROJ_1[[int, int]]

This uses the same syntax as for actual parameters, but doesn't mean the same thing, as the projections, injections, etc., are builtin, and not provided by any theories. Note that coercions don't work in this case, as PROJ_1::[[int, int] -> int] is the same as

    (LAMBDA (x: [[int, int] -> int]): x)(PROJ_1)
and not
    LAMBDA (x: [int, int]): PROJ_1(x)

The prover has been updated to handle extensionality and reduction rules as expected.

Coinductive definitions

Coinductive definitions are now supported. They are like inductive definitions, but introduced with the keyword `COINDUCTIVE', and generate the greatest fixed point.

Datatype updates

Update expressions now work on datatypes, in much the same way they work on records. For example, if lst: list[nat], then lst WITH [`car := 0] returns the list with first element 0, and the rest the same as the cdr of lst. In this case there is also a TCC of the form cons?(lst), as it makes no sense to set the car of null.

Complex datatypes with overloaded accessors and dependencies are also handled. For example,

  dt: DATATYPE
  BEGIN
   c0: c0?
   c1(a: (even?), b: int): c1?
   c2(a: nat, c: int): c2?
  END dt

  datatype_update: THEORY
  BEGIN
   IMPORTING dt
   x: dt
   y: int
   f: dt = x WITH [a := y]
  END datatype_update
This generates the TCC
f_TCC1: OBLIGATION
  (c1?(x) AND IF c1?(x) THEN even?(y) ELSE y >= 0 ENDIF) OR
   (c2?(x) AND IF c1?(x) THEN even?(y) ELSE y >= 0 ENDIF);

Datatype every

relation

If a top level datatype generates a map theory, the theory also contains an every relation. For lists, for example, it is defined as

  every(R: [[T, T1] -> boolean])(x: list[T], y: list[T1]):  boolean =
      null?(x) AND null?(y) OR
       cons?(x) AND
        cons?(y) AND R(car(x), car(y)) AND every(R)(cdr(x), cdr(y));
Thus, for example, if x and y are of type list[nat], then every(<)(x, y) returns true if the lists x and y are of the same length, and each element of x is less than the corresponding element of y.

Conversion messages

Messages related to conversions have been separated out, so that if any are generated a message is produced such as

  po_lems typechecked in 9.56s: 10 TCCs, 0 proved, 3 subsumed, 7 unproved; 4 conversions; 2 warnings; 3 msgs
In addition, the commands M-x show-theory-conversions and M-x show-pvs-file-conversions have been added to view the conversions.

More TCC information

Trivial TCCs of the form x /= 0 IMPLIES x /= 0 and 45 < 256 used to quietly be suppressed. Now they are added to the messages associated with a theory, along with subsumed TCCs. In addition, both trivial and subsumed TCCs are now displayed in commented form in the show-tccs buffer.

Numbers as constants

Numbers may now be declared as constants, e.g.,

  42: [int -> int] = LAMBDA (x: int): 42
This is most useful in defining algebraic structures (groups, rings, etc.), where overloading 0 and 1 is common mathematical practice. It's usually a bad idea to declare a constant to be of a number type, e.g.,
  42: int = 57
Even if the typechecker doesn't get confused, most users would.

Theory search

When the parser encounters an importing for a theory foo that has not yet been typechecked, it looks first in the .pvscontext file, then looks for foo.pvs. In previous versions, if the theory wasn't found at this point an error would result. The problem is that file names often don't match the theory names, either because a given file may have multiple theories, or a naming convention (e.g., the file is lower case, but theories are capitalized)

Now the system will parse every .pvs file in the current context, and if there is only one file with that theory id in it, it will be used. If multiple files are found, a message is produced indicating which files contain a theory of that name, so that one of those may be selected and typechecked.

NOTES