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. Tabular specifications of the kind advocated by Parnas are supported, with automated checks for disjointness and coverage of conditions. 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, and decision procedures for linear arithmetic.
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. The PVS Interface PVS uses Gnu or X Emacs to provide an integrated interface to its specification language and prover. Commands can be selected either by pull-down menus or by extended Emacs commands. Applications of PVS PVS is mainly intended for the formalization of requirements and design-level specifications, and for the analysis of intricate and difficult problems. Several examples are described in papers listed on the PVS home page.