[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

PVS 4.0 Release Notes

PVS 4.0 is available at http://pvs.csl.sri.com/download.shtml.

Release notes for PVS version 4.0.(1) The major difference from earlier versions of PVS is that this release is open source, under the GPL license. In addition, there is now a PVS Wiki page.

Installation Notes

Installation of binaries is the same as before; the only difference is that only one file needs to be downloaded. This leads to slightly more overhead when downloading for multiple platforms, but simplifies the overall process. Simply create a directory, untar the downloaded file(s) there, and run bin/relocate.

If you have received patches from SRI that you have put into your ~/.pvs.lisp file, they should be (re)moved. If you anticipate wanting to try the newer and older versions together, you can do this by using #-pvs4.0 in front of forms in your patches. This is a directive to the Lisp reader, and causes the following s-expression to be ignored unless it is an earlier version of PVS.

New Features

Open Source

PVS is now open source, under the under the GPL license. It currently builds with Allegro and CMU Common Lisps, and we are working on porting it to SBCL. Feel free to join in if your favorite Lisp or platform is not yet supported. See the PVS Wiki page for details.

Record and Tuple Type Extensions

Record and tuple types may now be extended using the WITH keyword. Thus, one may create colored points and moving points from simple points as follows.

  point: TYPE = [# x, y: real #]
  colored_point: TYPE = point WITH [# color: Color #]
  moving_point: TYPE = point WITH [# vx, vy: real #]

Similarly, tuples may be extended:

  R3: TYPE = [real, real, real]
  R5: TYPE = R3 WITH [real, real]

For record types, it is an error to extend with new field names that match any field names in the base record type. The extensions may not be dependent on the base type, though they may introduce dependencies within themselves.

  dep_bad: TYPE = point WITH [# z: {r: real | x*x + y*y < 1} #]
  dep_ok: TYPE = point WITH [# a: int, b: below(a) #]

Note that the extension is a type expression, and may appear anywhere that a type is allowed.

Structural Subtypes

PVS now has support for structural subtyping for record and tuple types. A record type S is a structural subtype of record type R if every field of R occurs in S, and similarly, a tuple type T is a structural subtype of a tuple type forming a prefix of T. Section Record and Tuple Type Extensions gives examples, as colored_point is a structural subtype of point, and R5 is a structural subtype of R3. Structural subtypes are akin to the class hierarchy of object-oriented systems, where the fields of a record can be viewed as the slots of a class instance. The PVS equivalent of setting a slot value is the override expression (sometimes called update), and this has been modified to work with structural subtypes, allowing the equivalent of generic methods to be defined. Here is an example.

points: THEORY
 point: TYPE+ = [# x, y: real #]
END points

genpoints[(IMPORTING points) gpoint: TYPE <: point]: THEORY
 move(p: gpoint)(dx, dy: real): gpoint =
  p WITH [`x := p`x + dx, `y := p`y + dy]
END genpoints

colored_points: THEORY
 Color: TYPE = {red, green, blue}
 colored_point: TYPE = point WITH [# color: Color #]
 IMPORTING genpoints[colored_point]
 p: colored_point
 move0: LEMMA move(p)(0, 0) = p
END colored_points

The declaration for gpoint uses the structural subtype operator <:. This is analogous to the FROM keyword, which introduces a (predicate) subtype. This example also serves to explain why we chose to separate structural and predicate subtyping. If they were treated uniformly, then gpoint could be instantiated with the unit disk; but in that case the move operator would not necessarily return a gpoint. The TCC could not be generated for the move declaration, but would have to be generated when the move was referenced. This both complicates typechecking, and makes TCCs and error messages more inscrutable. If both are desired, simply include a structural subtype followed by a predicate subtype, for example:

genpoints[(IMPORTING points) gpoint: TYPE <: point,
          spoint: TYPE FROM gpoint]: THEORY

Now move may be applied to gpoints, but if applied to a spoint an unprovable TCC will result.

Structural subtypes are a work in progress. In particular, structural subtyping could be extended to function and datatypes. And to have real object-oriented PVS, we must be able to support a form of method invocation.

Empty and Singleton Record and Tuple Types

Empty and singleton record and tuple types are now allowed in PVS. Thus the following are valid declarations:

Tup0: TYPE = [ ]
Tup1: TYPE = [int]
Rec0: TYPE = [# #]

Note that the space is important in the empty tuple type, as otherwise it is taken to be an operator (the box operator).


César Muñoz has kindly provided lisp code for PVSio, which has been fully incorporated into PVS. Thus for PVS 4.0 there is no need to download the package. See the doc/PVSio-2.d.pdf manual for details, and the PVSio web page http://research.nianet.org/~munoz/PVSio/ for updates.

Random Testing

We have developed a capability for random test generation in PVS, based, in part, on work done in Haskell and Isabelle. Random tests may be generated for universally quantified formulas in the ground evaluator or in the prover. In each case, the purpose is to try and find a counter example to the given formula, by evaluating a number of instances until one of them returns FALSE. The falsifying instance is then displayed.

This is a good way to test a specification before attempting a proof. Unlike model checking, it is inherently incomplete; on the other hand, there is no requirement for all types to be finite, only that all involved types and constants have interpretations.

For the prover, random testing is invoked with the random-test rule:

  (random-test &optional (fnum *) (count 10) (size 100)
               (dtsize 10) all? verbose? instance
               (subtype-gen-bound 1000))

In the ground evaluator, we added the test command:

  (test expr &optional (count 10) (size 100) (dtsize 10)
               all? verbose? instance)

Note one important difference: the optional arguments in the test command are not keywords. To set the all? flag you would need to invoke test as

  (test "foo" 10 100 10 t)

In general, random testing is most easily used in the prover. Note that you can get an arbitrary expression into the sequent by using the case command.

The count argument controls how many random tests to try. The size and dtsize control the possible ranges of random values, as described below. Normally the tests stop when a counter example is found; setting the all? flag to t causes further tests to be run until count is reached. The verbose? flag indicates that all random test values should be displayed. This is often useful to understand why a given test seems to always be true. The instance argument allows formals and uninterpreted types and constants to be given as a theory instance with actuals and mappings. The current theory may also be instantiated this way. For example, th[int, 0]{{T := bool, c := true}} may be a theory instance, providing actuals and mappings for the terms involved in the given formula. The subtype-gen-bound is used to control how many random values to generate in attempting to satisfy a subtype predicate, as described below.

In the prover, the universal formula is generated from the formulas specified by the fnum argument, first creating an implication from the conjunction of antecedents to the disjunction of consequents. Any Skolem constants are then universally quantified and the result passed to the random tester. This is useful for checking if the given sequent is worth proving; if it comes back with a counter example, then it may not be worth trying to prove. Of course, it may just be that a lemma is needed, or relevant formulas were hidden, and that it isn’t a real counter example.

The random values are generated per type. For numeric types, the builtin Lisp random function is used:

All other subtypes create a random value for the supertype, and then check if it satisfies the subtype predicate. It stops after subtype-gen-bound attempts. Higher-order subtypes such as surjective? are not currently supported. Function types generate a lazy function, so that, e.g.,

    FORALL (f: [int -> int], x, y, z: int):
       f(x) + f(f(y)) > f(f(f(z)))

creates a function that memoizes its values. Other types (e.g., record and tuple types) are built up recursively from their component types.

Datatypes are controlled by dtsize. For example, with size and dtsize set to their defaults (100 and 10, respectively), a variable of type list[int] will generate lists of length between 0 and 10, with integer values between -100 and 100.

More details may be found in the paper Random Testing in PVS, which was presented at AFM 2006.


New prover commands are available that invoke the Yices SMT solver. See http://yices.csl.sri.com for details on Yices and its capabilities. You must download Yices from there and include it in your PATH, as it is not included with PVS. You will get a warning on starting PVS if Yices is not found in your path, but this can safely be ignored if you will not be using Yices.

The yices rule is an endgame solver; if it does not prove (the specified formulas of) the sequent, it acts as a skip. In addition to the primitive yices rule, the strategies yices-with-rewrites and ygrind have been added. Use help (e.g., (help ygrind)) for details.

Recursive Judgements TCCs

Judgements on recursive functions often lead to difficult proofs, as one generally has to prove the resulting obligation using tedious induction. For example, here is a definition of append on lists of integer, and a judgement that it is closed on lists of natural numbers (note that this example is artificial; append is defined polymorphically in the prelude):

 append_int(l1, l2: list[int]): RECURSIVE list[int] =
    CASES l1 OF
      null: l2,
      cons(x, y): cons(x, append_int(y, l2))
    MEASURE length(l1)
 append_nat: JUDGEMENT append_int(a, b: list[nat]) HAS_TYPE list[nat]

This yields the TCC

append_nat: OBLIGATION
  FORALL (a, b: list[nat]):
    every[int]({i: int | i >= 0})(append_int(a, b));

Which is difficult to prove automatically (or even manually).

By adding the keyword RECURSIVE to the judgement, the TCCs are generated by

With these changes, the TCC becomes

append_nat_TCC1: OBLIGATION
  FORALL (a, b: list[nat], x: int, y: list[int]):
    every({i: int | i >= 0})(append_int(a, b)) AND a = cons(x, y)
     every[int]({i: int | i >= 0})(cons[int](x, append_int(y, b)));

and this is easily discharged automatically (e.g., with grind).

Note that recursive judgements are used in exactly the same way as the non-recursive form; the only difference is in the generated TCCs.

Recursive judgements are only allowed on recursive functions, and they are only for closure conditions (i.e., arguments must be provided). If a non-recursive judgement is given where a recursive judgement would apply, then a warning is output. In general, recursive judgements are preferred. In fact, we considered making it the default behavior for judgements on recursive functions, but this would make existing proofs fail.

Prelude Additions

To support the Yices interface, several operators from the bitvector library have been moved to the prelude. These are in the new theories floor_div_props, mod, bv_arith_nat_defs, bv_int_defs, bv_arithmetic_defs, and bv_extend_defs. The floor_div_props and mod theories have been moved completely, the rest have only had the operators added to the prelude - the rest of the theory, along with lemmas and other useful declarations, is still in the bitvector library - just drop the _def for the corresponding theory.

Note that this can have some side effects. For example, the WIFT tutorial adder example expects conversions to be used in a certain way because there were no arithmetic operators on bit vectors. Now that there are such operators, conversions no longer are needed, and proofs obviously fail.

Decimal Representation for Numbers

PVS now has support for decimal representation of numbers, for example, 3.1416. Internally, this is treated as a fraction, in this case 31416/10000. So there is no floating point arithmetic involved, and the results are exact, since Common Lisp represents fractions exactly. The decimal representation must start with an integer, i.e., 0.007 rather than .007.

Unary +

The + operator may now be used as a unary operator. Note that there is no definition for unary +, for example, +1 will lead to a type error. This was added primarily for user declarations.

Bug Fixes

This version fixes many (though not all) bugs. Generally those marked as analyzed in the PVS bugs list have been fixed, and most have been incorporated into our validation suite.


There were some improvements made to judgements and TCC generation, that in some cases lead to different forms of TCCs. In the validation suite, these were all easily detected and the proofs were not difficult to repair.

It was noted in bug number 920 that the instantiator only looks for matches within the sequent, though often there are matches from the Skolem constants that are not visible. The inst? command was modified to look in the Skolem constants as a last resort, so earlier proofs would still work. Unfortunately, grind and similar strategies use inst? eagerly, and may now find a Skolem constant match that is incorrect, rather than waiting for a better match after further processing. This is exactly the problem that lazy-grind was created for. In our validation suite only a few formulas needed to be repaired, and those generally could be fixed simply by replacing grind by lazy-grind. Since hidden Skolem constants are difficult for a new user to deal with, we feel that this is a worthwhile change.

[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by Sam Owre on February 11, 2013 using texi2html 1.82.