| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 | ||
| New Features | ||
| Bug Fixes | ||
| Incompatibilities |
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.
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 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.
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
BEGIN
point: TYPE+ = [# x, y: real #]
END points
genpoints[(IMPORTING points) gpoint: TYPE <: point]: THEORY
BEGIN
move(p: gpoint)(dx, dy: real): gpoint =
p WITH [`x := p`x + dx, `y := p`y + dy]
END genpoints
colored_points: THEORY
BEGIN
IMPORTING points
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 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.
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:
nat uses random(0..size)
int uses random(-size..size)
rat creates two random ints, the second nonzero,
and returns the quotient
real and above just use rat values
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.
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))
ENDCASES
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
every({i: int | i >= 0})(append_int(a, b)).
list[nat]), with the predicate as a condition.
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)
IMPLIES
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.
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.
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.
+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.
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.