Home | • | Intro | • | Wiki | • | Docs | • | FAQ | • | Download | • | Bugs | • | • | FM Tools |
---|

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

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

- Allegro 6.0 Port
- Theory interpretations
- Multiple proofs
- Library relative pathnames
- Cotuple types
- Coinductive definitions
- Datatype updates
- Datatype
`every`relation - Conversion messages
- More TCC information
- Numbers as constants
- Theory search

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 are described fully in Theory Interpretations in PVS

- This introduces one backward incompatible change; theory
abbreviations such as
foo: THEORY = bar[int, 3]

should be changed to the new formIMPORTING bar[int, 3] AS foo

Note that ``AS`' is a new keyword, and may cause parse errors where none existed before. - The stacks example doesn't work as given; in particular, the
mappings for
`push`,`top`, and`pop`should be changed topush := LAMBDA (x: t, A: E[cstack, ce]): equiv_class[cstack,ce](cpush(x)(rep(A))), top := LAMBDA (A: E[cstack, ce] | cnonempty?(rep(A))): ctop(rep(A)), pop := LAMBDA (A: E[cstack, ce] | cnonempty?(rep(A))): equiv_class[cstack,ce](cpop(rep(A)))

Otherwise unprovable TCCs result (e.g., every stack is nonempty).

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 |

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.

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_1This 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 are now supported. They are like inductive
definitions, but introduced with the keyword ``COINDUCTIVE`', and
generate the greatest fixed point.

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_updateThis 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);

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

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 msgsIn addition, the commands

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 may now be declared as constants, e.g.,

42: [int -> int] = LAMBDA (x: int): 42This 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 = 57Even if the typechecker doesn't get confused, most users would.

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.

- Once a file has been typechecked, the
`.pvscontext`is updated accordingly, and this check is no longer needed. `.pvs`files that contain parse errors will be ignored.

Home | • | Intro | • | Wiki | • | Docs | • | FAQ | • | Download | • | Bugs | • | • | FM Tools |
---|

*
Last modified: Thu 30 Nov 2006 12:15 UTC
Maintainer: Sam Owre
*