PVS is a large, complex system; here we give a high level description of the language, prover, user interface, and other features of PVS. Details may be found in the documentation
The specification language of PVS is based on classical, typed higher-order logic. The base types include uninterpreted types that may be introduced by the user, and built-in types such as the booleans, integers, reals, and the ordinals up to epsilon_0; the type-constructors include functions, sets, tuples, records, enumerations, and inductively-defined abstract data types, such as lists and binary trees, and coinductively-defined abstract data types such as streams. Predicate subtypes and dependent types can be used to introduce constraints, such as the type of prime numbers or order-preserving maps. These constrained types may incur proof obligations (called type-correctness conditions or TCCs) during typechecking, but greatly increase the expressiveness and naturalness of specifications. In practice, most of the obligations are discharged automatically by the theorem prover. PVS specifications are organized into parameterized theories that may contain assumptions, definitions, axioms, and theorems. Parameters can include constants, types, and theory instances. Theory interpretations are used to instantiate the declared types and constants in a theory with definitions. Theory interpretations can be used for exhibiting models for an axiomatic theory and to refine a abstract theory in terms of a concrete one. Definitions are guaranteed to be conservative extensions; to ensure this, recursive function definitions generate termination proof obligations. Inductively-defined relations are also supported. PVS expressions provide the usual arithmetic and logical operators, function application, lambda abstraction, and quantifiers, within a natural syntax. Names may be freely overloaded, including those of the built-in operators such as AND and +. Tabular specifications of the kind advocated by Parnas are supported, with automated checks for disjointness and coverage of conditions. An extensive prelude of built-in theories provides hundreds of useful definitions and lemmas; user-contributed libraries provide many more.
The PVS theorem prover provides a collection of powerful primitive inference procedures that are applied interactively under user guidance within a sequent calculus framework. The primitive inferences include propositional and quantifier rules, induction, rewriting, simplification using decision procedures for equality and linear arithmetic, data and predicate abstraction, and symbolic model checking. The implementations of these primitive inferences are optimised for large proofs: for example, propositional simplification uses BDDs, and auto-rewrites are cached for efficiency. User-defined procedures can combine these primitive inferences to yield higher-level proof strategies. There is a synergistic interaction between the PVS language features and the prover so that the type information associated with a term is exploited by the inference mechanisms, and conversely, the automation in the prover is helpful in automatically discharging TCCs. Proofs yield scripts that can be edited, attached to additional formulas, and rerun. This allows many similar theorems to be proved efficiently, permits proofs to be adjusted economically to follow changes in requirements or design, and encourages the development of readable proofs.
PVS includes a BDD-based decision procedure for the relational mu-calculus and thereby provides an experimental integration between theorem proving and CTL model checking. PVS has recently been extended to use the Yices SMT solver as an endgame prover and an infinite-state bounded model checker, the PVSio framework for evaluating ground PVS expressions, and a random testing capability that can be used during proofs.
PVS provides a suite of tools for non-interactive proof checking. These tools enable a semi-literate proving style where specification and proof scripts reside in the same file (as it is done in Coq and other proof assistants).
These tools include:
PVSio is the animation environment of PVS, provided by NASA Langley. It is built into PVS, on top of the ground evaluator, which generates Common Lisp code from PVS functional specifications to evaluate ground expressions within the underlying PVS Common Lisp environment. PVSio provides a predefined library of imperative programming language features such as side effects, unbounded loops, input/output operations, floating point arithmetic, exception handling, pretty printing, and parsing.
The current version of PVSio provides:
PVSio-web is a graphical environment that transforms the animation capabilities of the standard PVS theorem proving system with a sophisticated graphical front-end allowing interactive (human-computer) systems modelling and prototyping. This is not built in to PVS, see the above link for installation instructions. Using PVSio-web, one can generate and evaluate realistic interactive prototypes from formal models. PVSio-web has been successfully used over the last two years for analysing commercial medical devices, and has been used to create training material for device developers and device users. For safety-critical medical device design, PVSio-web has been used with formal methods experts and with non-technical end users, including doctors and nurses.
