A pvs – An Introduction Edmund Clarke

15-820A PVS – An Introduction

• Edmund Clarke

• Daniel Kroening

• Carnegie Mellon University

Outline

• Theorem provers

• Why PVS?

• Topics for this semester

• Short introduction to the PVS language

• The PVS workflow

• A short proof

Theorem Provers

• Stores theorems and establishes their correctness

• What kind of theorems?

• First order
• Second order / higher order

• How to establish the correctness?

• Completely automated
• Semi-automated
• Interactive (manual)

Theorem Provers

• There is a wide range of theorem

• provers

• Higher order: ALF, Alfa, Coq, HOL, PVS

• Logical Frameworks: Isabelle, LF, Twelf

• Inductive: ACL2, Inka

• Automated: Gandalf, TPS, Otter, Setheo, SPASS

• EQP, Maude

Theorem Provers

• The most commonly used Theorem Provers, from systems verification point of view

• HOL: Floating Point Verification (Intel)
• ACL2: Floating Point Verification (AMD)
• PVS: NASA/DoD, e.g., Space Shuttle flight control requirements specification It also does Floating Point Units.

• PVS is…

• Higher order
• Interactive

PVS Workflow

Why PVS?

• Why PVS and not some other theorem prover?

Why PVS?

• Why PVS and not some other theorem prover?

• Other (strong) theorem provers probably worse

• The PVS language is close to “normal” notation

• Not LISP!

• PVS is interactive – why not an automated theorem prover?

• Decidable logics often not rich enough, or inconvenient
• Semi-automated theorem provers usually don’t tell what is wrong, experience and knowledge about internals required

Topics for this Semester

• PVS

• Installation
• Proof Interaction

• Language Basics

• Types
• Type Checking
• Recursion
• Lambda Notation
• Abstract Data Types

Topics for this Semester

• Specification using PVS

• Prelude, Libraries
• State Machines
• Tabular Specifications
• How to get “systems” into PVS
• Hardware
• Software

Topics for this Semester

• Proofs

• Induction
• Real Numbers
• Abstraction of Infinite State Transition Systems

• Proof Automation

• Rewriting
• Write your own decision procedure!
• Model Checking as Rule of Inference

The PVS Language

• There are two languages

• The language to write definitions and theorems (“definition language“)
• The language to prove theorems (“proof language”)
• They have nothing to do with each other

• The definition language looks like “normal math” (translator to Latex built in)

• The proof language looks like LISP

The PVS Definition Language

• Main language elements

• Declarations
• Types
• Constants
• Expressions over these types
• Expressions of Boolean types may be a formula
• Formulae are theorems or axioms
• Declarations and formulae are grouped into theories

The PVS Definition Language

The PVS Definition Language

The PVS Definition Language

Axioms vs. Theorems

• Axioms are assumed to be true

• Dangerous!

• Avoid axioms, use constant declarations instead:

Types

• PVS has a very rich type concept

• Uninterpreted type declaration:
• numbers: TYPE
• numbers: NONEMPTY_TYPE
• Interpreted type declaration Introduce names for type expressions
• posint: TYPE={ i: integer | i > 0}

Types PVS comes with

• boolean

• FALSE, TRUE

• Number types

• real, rational, integer, natural

• string

• Ordinals

Type Expressions

• Function Types

• [ t1,…,tn -> t ]
• Sugar for that:
• FUNCTION[ t1,…,tn -> t ]
• ARRAY[ t1,…,tn -> t ]
• Note that ti and t may be function types as well!

Expressions

• Constants

• Given by their name, as used in the declaration
• Numbers (1, 2, 3, …) are actually identifiers and can even be overloaded
• If name is ambiguous, use
• identifier::type

Expressions

• Function Applications

• f(x)
• Tons of Syntactic sugar for that, don’t be confused
• Binary operator symbols
• y * z is the same as *(y, z)

Expressions

• Functions PVS comes with

• Boolean
• AND &, OR, IMPLIES =>,
• WHEN, IFF <=>
• IF c THEN a ELSE b
• IF: [boolean, T, T -> T]
• (COND: sugar for IF THEN ELSE)
• Numeric operators
• +, -, *, /, ^, <, <=, >, >=

Expressions

• Binding Expressions

• Quantifiers
• EXISTS (x: T): p(x)
• FORALL (y: T): q(y)

Expressions

• Binding Expressions

• Lambda: unnamed functions
• LAMBDA (x: int): x+1
• Type of that: [ int -> int ]

Recursion

• Lambda cannot be used for recursion

• Only named functions allow recursion

• No mutual recursion

Expressions

• LET Expressions

• LET i:T=e1 IN e2
• Useful for avoiding redundancy if e1 is used many times in e2
• Sugar for LAMBDA
• (LAMBDA (i: T): e2)(e1)
• Example
• LET x=2 IN x*y
• is
• (LAMBDA x: x*y)(2)

Expressions

• Override Expressions

• e WITH [(i1):=v1, (i2):=v2, …]
• Sugar for LAMBDA
• LAMBDA x: IF x=i1 THEN v1 ELSIF x=i2 THEN v2 … ELSE e(x) ENDIF
• Also for records and tuples

Expressions

• LET and WITH useful for some sequential program constructs!

Expressions

• Set Expressions

• In PVS, sets are represented using their characteristic function
• [ T -> boolean ] same as setof[T]
• Set expressions:
• { x:T | p(x) }
• For sets a, b over T:
• Union: a OR b
• Intersection: a AND b

Some Syntactic Sugar

• Tuple types

• [ t1,…,tn ]

• Tuple expressions

• ( e1,…,en )

• Comes with projections

• PROJ_1, PROJ_2, ..., PROJ_n

Example

Some Syntactic Sugar

• Record types

• [# a1:t1,…,an:tn #]

• Record expressions

• (# a1:=e1,…,an:=en #)

• Comes with projections

• a1, a2, ..., an

• Or: e`ai

Example

Subtypes

• { x: T | p(x)}

• p must be of type [ T -> boolean ]

• Sugar for that:

• (p)

• This type contains all elements x of T for which p(x) is true

• E.g., define domain of integer division:

• { x: integer | x/=0 }

• Makes type equivalence undecidable

Subtypes

• Subtypes in binding expressions

• Forall, exists: forall (i: int | i>10): …
• Lambda:

Example

Example

Example

Proof?

• How to argue?

• pop(push(x, s)) = s

• Let’s to the size component and the elements component separately

• Size:

• pop(push(x, s))`size = s`size

• Expand definition of pop:

• push(x, s)`size - 1 = s`size

• Expanding the definition of push results in

• s`size+1-1=s`size

Proof? (2)

• Elements:

• pop(push(x, s))`elements = s`elements

• Expand definition of pop:

• ((j:nat|j
  

• Expanding the definition of push results in

• ((j:nat|j

• Obviously, the condition of the IF is always true

What next…

• Webpage!

• Installation instructions for PVS
• Further reading
• Homework assignment