PVS Tutorial Introduction, April 1993 Introduction to Mechanically-Supported Formal Methods

Using PVS

Sam Owre, John Rushby, N. Shankar

Computer Science Laboratory SRI International Menlo Park CA USA

PVS: Prototype Verification System

• Verification System: specification language and associated mechanization (parser, typechecker etc.), plus a theorem prover or proof checker

• Our main system is EHDM: stands for Enhanced HDM (and HDM stands for Hierarchical Development Methodology); work on EHDM started in 1983 and it has been through many revisions since then

• Ehdm was built for a US government agency and has restricted availability (US only)

• Work on PVS started in 1990

• Built to prototype new theorem prover for EHDM

PVS: People’s Verification System

• PVS was also built to be widely available (SRI-funded and owned)

• It’s free

• You can get it by anonymous FTP from

    ftp.csl.sri.com in /pub/pvs

(Allegro lisp implementation for Sun SparcStations)

• Recommend 32M real memory, 100M swap space, Sparc 2 or better

• Also available in Lucid Lisp for Sparcs, DEC, IBM workstations (have to buy Lucid license)

• Still evolving: this is a beta release

PVS Users and Proofs

• NASA Langley, NASA Johnson, IBM FSD, Jet propulsion Lab Requirements definition project for part of Space Shuttle on-orbit control system

• A manufacturer of flight-control systems Microcode verification for an avionics processor

• Ourselves ∘ Pipeline correctness (Mini-Cayuga, Saxe) ∘ Simple microcode correctness (Tamarack) ∘ Real-time arguments

(Fischer mutual-exclusion, railroad crossing) ∘ Byzantine agreement protocols

(Oral Messages, Hybrid Oral Messages) ∘ The Boyer-Moore fast majority algorithm, MJRTY ∘ Standard math and CS test cases

(Schröder-Bernstein, ordered binary tree insertion etc.)

PVS Tutorial Intro 4

Why Mechanize Formal Methods?

• An unchecked formal specification is no more likely to be correct than an untested program or gate layout ∘ Need strong checks on internal consistency to make sure it

says something ∘ Then must validate to make sure it says what is intended

Primarily by challenging the specification

(posing putative theorems to explore their consequences) Requires mechanization to do this reliably

• To contribute to assurance, formal methods should focus on the things that go wrong: typically the hardest parts of the design (at least in industries with established V&V) ∘ Concurrency, distribution, fault-tolerance ∘ Need to prove hard theorems Requires mechanization to do this reliably

Proofs or Theorems?

• Proofs are less instruments of justification than tools of discovery

• A mechanized proof-checker is not an oracle, but an implacable skeptic “The virtue of a logical proof is not that it compels belief but that it suggests doubts” [Lakatos]

• Proofs expose assumptions

• And help develop insight

• It’s not enough just to get theorems proved, you want beautiful proofs

Design Goals for PVS

• Want an attractive, expressive specification language

• Want effective mechanized support

∘ Without mechanization, formal methods are just

documentation ∘ Strong, early error detection ∘ A theorem prover with real muscle ∘ That helps develop understanding

The Three Traditions

• Historically, these requirements have been in conflict: the most effective theorem provers are associated with the most impoverished notations, and vice-versa • Specification languages: choose an expressive notation

without concern for its mechanization, then try to mechanize (VDM, Z, Raise)

• Theorem provers: choose a theorem prover, then use its logic as a specification language (Nqthm, Otter, RRL)

• Integrated verification systems: make compromises on language and theorem prover to get coherent system (Gypsy, FDM, HOL, HDM, EHDM, PVS, Imps, Eves)

[figure: Integrated; Verification; Systems; Theorem; Provers; Specification; Notations; Theorem Proving Effectiveness; s; s; e; n; e; v; i; s; s; e; r; p; x; E; Systems; Really Useful]

Design Philosophy of PVS

• Language and theorem proving issues have to be solved together

• If you assume a decent prover, can contemplate novel strategies: Allow the type system to become undecidable (so typechecking requires theorem proving)

• If you assume an expressive language, theorem proving will require guidance from the user Must retain formulas in original form

Looking for a Foundation

• Formal logics were developed to explore the underpinnings of mathematics

• Optimized for metamathematical convenience: proof of completeness and consistency theorems

• Mathematicians content that mathematical theories can be formalized “in principle”—they never actually do it

• Similarly, for formal proofs

• In formal methods for computer science, we want to formalize theories in practice, and do mechanically-checked proofs for real

• Should take inspiration from traditional logics and formal proof methods, but little else

Choosing a Foundation

• First order predicate calculus is much too limited

• First order set theory requires a lot of metamathematical assistance and crafty encodings (everything is a set)

• Unrestricted higher-order set theory is unsound

• Typed logics provide clarity, discipline, early error detection

• Typed set theory has very difficult semantics And functions are inherently partial in set theory (an obstacle to efficient theorem proving)

• Simple theory of types (ordinary higher-order logic) provides most of what you need (functions are first-class citizens: quantification allowed over functions and predicates as well as individuals, and functions may take functions as arguments and return them as values)

• Embellishing the type system provides the rest

PVS Tutorial Intro 12

Design Choices in PVS: 1

• A specification language is a logic Issues such as executability, connection to a programming language, are secondary

• A typed logic provides clarity, discipline, early error detection • No set theory: use higher-order logic and identify sets with

predicates (axiom of comprehension is sound in higher-order logic because of the typing restrictions)

• No partial functions: extend type system with predicate subtypes and dependent types

• No state: encode computational models within higher-order logic

• No polymorphism: parameterized theories

• No schemas: theories with semantic constraints • Allow axioms

(later, provide way to demonstrate their consistency)

• But also provide definitional forms that guarantee conservative extension ∘ (Recursive) function definitions ∘ Datatypes

• Types must include standard computer-science constructions ∘ Tuples ∘ Records ∘ Sets ∘ Numbers • Keep the system lean and mean

• Build on standard interfaces: Unix, Gnu Emacs, LaTEX

• Provide facilities for managing large specifications: browsing and searching, prettyprinting, typesetting

• Context retained from one session to another

• Status commands to keep track of development

• Not required to do things in order (can postpone proof obligations)

• You need a theorem prover to do theorem proving!

• Powerful primitive inferences: uses decision procedures, rewriter, simplification, type information in an integrated manner

• Direct control by the user at the higher-levels

• Sequent calculus presentation

• Strategy language to allow user extensions

• Not required to do things in order (can use lemmas before proving them)

• Proofs saved in a robust form, can be rerun automatically