A pvs – An Introduction Edmund Clarke



Yüklə 469 b.
tarix18.08.2018
ölçüsü469 b.
#72958


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



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



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



What next…

  • Webpage!

    • Installation instructions for PVS
    • Further reading
    • Homework assignment


Yüklə 469 b.

Dostları ilə paylaş:




Verilənlər bazası müəlliflik hüququ ilə müdafiə olunur ©muhaz.org 2024
rəhbərliyinə müraciət

gir | qeydiyyatdan keç
    Ana səhifə


yükləyin