| | | | |
|
FME '96 Tutorial: An Introduction to Some Advanced Capabilities of PVS
by Sam Owre & Dr. John Rushby.
Abstract
The specification language of PVS builds on classical higher-order logic and the simple theory of types. PVS extends simple type theory with dependent types and predicate subtypes, structures specifications into parameterized theories, and adds a construction for freely generated abstract data types. These extensions provide a surprisingly rich set of capabilities, and the purpose of this tutorial is to introduce some of them to you. The strategy mechanism of the PVS theorem prover likewise allows rather powerful capabilities to be built on the basic theorem proving resources of propositional calculus, quantifier reasoning, decision procedures, and rewriting; some of these capabilities are also described here.
Files
|
|
|