PVS Tutorial

PVS Tutorial

Sam Owre, John Rushby, and N. Shankar

Computer Science Laboratory

SRI International Menlo Park CA USA

PVS System

• Uses Emacs as its interface

• PVS Functions available as Emacs commands

(e.g., M-x prove)

• Functions ∘ Parse, prettyprint, L^{A}TEX-print ∘ Typecheck ∘ Prove ∘ Edit and rerun proofs ∘ Status and proof-chain analysis ∘ Browsing functions

Example: Phone Book I

phone1 : THEORY
BEGIN
N: TYPE              % names
P: TYPE              % phone numbers
B: TYPE = [N -> P]   % phone books
n0: P
nm, x: VAR N
pn: VAR P
bk: VAR B
emptybook: B
emptyax: AXIOM emptybook(nm) = n0
FindPhone: [B, N -> P]
Findax: AXIOM FindPhone(bk,nm) = bk(nm)
AddPhone: [B, N, P -> B]
Addax: AXIOM AddPhone(bk,nm,pn)(x) =
               IF x = nm THEN pn ELSE bk(x) ENDIF
DelPhone: [B, N -> B]
Delax: AXIOM DelPhone(bk,nm)(x) =
               IF x = nm THEN n0 ELSE bk(x) ENDIF
FindAdd: LEMMA FindPhone(AddPhone(bk,nm,pn),nm) = pn
DelAdd: LEMMA DelPhone(AddPhone(bk,nm,pn),nm) = bk
END phone1

Example: Phone Book I(a)

phone1 : THEORY
BEGIN
N: TYPE              % names
P: TYPE              % phone numbers
B: TYPE = [N -> P]   % phone books
n0: P
nm, x: VAR N
pn: VAR P
bk: VAR B
emptybook(nm): P = n0
FindPhone(bk,nm): P = bk(nm)
AddPhone(bk,nm,pn)(x): P = IF x = nm THEN pn ELSE bk(x) ENDIF
DelPhone(bk,nm)(x): P = IF x = nm THEN n0 ELSE bk(x) ENDIF
FindAdd: LEMMA FindPhone(AddPhone(bk,nm,pn),nm) = pn
DelAdd: LEMMA DelPhone(AddPhone(bk,nm,pn),nm) = bk
END phone1

Example: Phone Book II

phone2 : THEORY
BEGIN
N: TYPE              % names
P: TYPE              % phone numbers
B: TYPE = [N -> setof[P]]   % phone books
nm, x: VAR N
pn: VAR P
bk: VAR B
emptybook: B = (LAMBDA nm: emptyset[P])
FindPhone(bk,nm): setof[P] = bk(nm)
AddPhone(bk,nm,pn): B =
   (LAMBDA x: IF x = nm THEN union(bk(nm),singleton(pn))
              ELSE bk(x) ENDIF)
DelPhone(bk,nm): B =
   (LAMBDA x: IF x = nm THEN emptyset[P] ELSE bk(x) ENDIF)
DelPhoneNum(bk,nm,pn): B =
   (LAMBDA x: IF x = nm THEN difference(bk(nm),singleton(pn))
              ELSE bk(x) ENDIF)
FindAdd: LEMMA member(pn,FindPhone(AddPhone(bk,nm,pn),nm))
DelAdd: LEMMA DelPhoneNum(AddPhone(bk,nm,pn),nm,pn) =
              DelPhoneNum(bk,nm,pn)
END phone2

Example: Phone Book III

phone3 : THEORY
BEGIN
N: TYPE                           % names
P: TYPE                           % phone numbers
B: TYPE = [N -> setof[P]]         % phone books
VB: TYPE = {b:B | (FORALL (x,y:N): x /= y => disjoint?(b(x), b(y)))}
nm, x: VAR N
pn: VAR P
bk: VAR VB
emptybook: VB = (LAMBDA (x:N): emptyset[P])
FindPhone(bk,nm): setof[P] = bk(nm)
UnusedPhoneNum(bk,pn): bool =
   (FORALL nm: NOT member(pn,FindPhone(bk,nm)))
AddPhone(bk,nm,pn): VB =
   (LAMBDA x: IF x = nm AND UnusedPhoneNum(bk,pn)
                 THEN union(bk(nm),singleton(pn))
              ELSE bk(x) ENDIF)

Example: Phone Book III (continued)

DelPhone(bk,nm): VB =
   (LAMBDA x: IF x = nm THEN emptyset[P] ELSE bk(x) ENDIF)
DelPhoneNum(bk,nm,pn): VB =
   (LAMBDA x: IF x = nm THEN difference(bk(nm),singleton(pn))
              ELSE bk(x) ENDIF)
FindAdd: LEMMA UnusedPhoneNum(bk,pn) IMPLIES
                 member(pn,FindPhone(AddPhone(bk,nm,pn),nm))
DelAdd: LEMMA DelPhoneNum(AddPhone(bk,nm,pn),nm,pn) =
              DelPhoneNum(bk,nm,pn)
END phone3

Example: Phone Book III TCCs

emptybook_TCC1: OBLIGATION
(FORALL (x, y: N): x /= y => disjoint?[P](emptyset[P], emptyset[P]))
AddPhone_TCC1: OBLIGATION
(FORALL nm, bk, pn, (x, y: N):
x /= y =>
disjoint?[P](IF x = nm AND UnusedPhoneNum(bk, pn)
  THEN union[P](bk(nm), singleton[P](pn))
ELSE bk(x) ENDIF,
IF y = nm AND UnusedPhoneNum(bk, pn)
  THEN union[P](bk(nm), singleton[P](pn))
ELSE bk(y) ENDIF))
DelPhone_TCC1: OBLIGATION
(FORALL nm, bk, (x, y: N):
x /= y =>
disjoint?[P](IF x = nm THEN emptyset[P] ELSE bk(x) ENDIF,
IF y = nm THEN emptyset[P] ELSE bk(y) ENDIF))
DelPhoneNum_TCC1: OBLIGATION
(FORALL nm, bk, pn, (x, y: N):
x /= y =>
disjoint?[P](IF x = nm THEN difference[P](bk(nm), singleton[P](pn))
ELSE bk(x) ENDIF,
IF y = nm THEN difference[P](bk(nm), singleton[P](pn))
ELSE bk(y) ENDIF))

Types

• Built-in ground types:

number, real, rational, integer, nat, bool

• New uninterpreted types:

foo, T: TYPE

• Enumeration types:

colors:  TYPE = {red, blue, green}

• Function types (keyword FUNCTION is optional, functions with range bool are sometimes called predicates or relations and also represent sets):

stackpred:  TYPE = [stack -> bool]
stackpred:  TYPE = predicate[stack]
stackpred:  TYPE = setof[stack]

• Type synonyms:

primaries:  TYPE = colors

Constants, Variables

• Uninterpreted constants:

bar, c:  foo
exp:  [nat, nat -> nat]
isempty:  stackpred
isempty:  predicate[stack]

• Variables:

x, y:  VAR nat
fun:  VAR [T1 -> T2]

Expressions

• Literals: numerics (e.g., 10, -24), truth values TRUE, FALSE, and enumeration constants

• Identifiers: of constants and variables (all names can be overloaded)

• Logical connectives:

         AND, &, OR, NOT, IMPLIES, =>, WHEN, IFF, <=>, =, /=

• Polymorphic if-then-else:

         IF ...  THEN ...  ELSE ...  ENDIF

• Arithmetic operators and relations:

         +, -, *, /, <, <=, >, >=

Expressions (Continued)

• Function application

foo(x, y)
goo(a, b)(c)

• LET expression allows local naming of long expressions

(also WHERE & PLET):

LET x = ..., y = ...  IN f(x, y) + g(x, y)

• Quantifiers:

(FORALL x, y:  ...  )
(EXISTS x, y:  ...  )

Free variables treated as universally quantified

Definitions, Axioms, Lemmas

• Interpreted (defined) constants:

max:  nat = 10
abs((x:int)):nat = IF x < 0 THEN -x ELSE x ENDIF

• Axioms:

foo:  AXIOM n <= 3 * m
deadly:  AXIOM (FORALL e, s:  push(e, s) = newstack)

• Theorems: many keywords can be used—i.e., THEOREM, LAW,

LEMMA, SUBLEMMA, COROLLARY, PROPOSITION, FACT, CLAIM,
CONJECTURE, FORMULA
stackprop:  LEMMA top(pop(push(e, s))) = top(s)

Theories

• Theories provide packaging, control of visibility

• Parameterization supports reuse, provides limited dependent typing

• Theories: can be parameterized by types and constants

stacks[elemtype:TYPE, undef:elemtype] :  THEORY

• Continues with

[EXPORTING ...]
BEGIN
[ASSUMING ...  ENDASSUMING]
...
END stacks

• Can be imported into another theory uninstantiated:

IMPORTING stacks

• Or instantiated:

IMPORTING stacks[nat, 0]

• IMPORTINGs may appear where declarations are allowed

pvscourse 14

Disambiguating Names

• Names from imported theories can be given in full:

         stacks[nat, 0].stack

• Or abbreviated:

         stack[nat, 0]

• Or often inferred from context:

         stack

Exporting Names

• By default all names are exported—same as

         EXPORTING ALL WITH CLOSURE

• Limit visibility by explicitly listing those to be exported

(before the BEGIN):

         EXPORTING foo, bar

• Can re-export imported names:

         IMPORTING foo
         EXPORTING goo WITH foo

• Re-exported theories must be fully instantiated

Function Constants

• Lambda notation is used to define function constants

(Variables e and s must have been declared earlier):

(LAMBDA e, s:  push(e, pop(s)))

• Types of variables may be locally declared:

(LAMBDA (e:elemtype), (s:stack):  push(e, pop(s)))

• Lambda expressions can be used anywhere a function

constant is expected:

replace:  [elem, stack -> stack] =
   (LAMBDA e, s:  push(e, pop(s)))
obvious:  LEMMA (LAMBDA x:  x+1)(y) - 1 = y

• Set notation can be used instead of LAMBDA if range type is

bool:
{ x | (EXISTS y:  x = 2*y) }

Function Definitions

• There are lots of equivalent ways of defining functions:

   ∘ foo:  [int -> [int, int -> int]] =
            (LAMBDA (x:int):(LAMBDA (y, z:int):  x + y * z))
   ∘ foo((x:int)):  [int, int -> int] =
            (LAMBDA (y, z:int):  x + y * z)
   ∘ foo((x:int))((y,z:int)):  int = x + y * z
   ∘ foo(x)(y,(z:int)):  int = x + y * z
   ∘ foo(x)(y,z):  int = x + y * z

• Defining expression must be closed (no free variables)

• These are all syntactic sugar for the first form

• The last form is generally the most convenient

• Note: if a local binding is not provided, the variable must be declared earlier in the theory.

• PVS definitions guarantee conservative extension

pvscourse 18

Functions (Summary)

• Type declaration:

         fun:  [int, [nat -> nat] -> [nat -> int]]

• Application:

         fun(3, suc)(x)

• Literal constant:

         (LAMBDA x, f:  (LAMBDA n :  f(n)+x))

Tuples

• Type declaration:

         tup:  [int, bool, [nat -> nat]]

• Dereferencing:

         proj 2(tup)

• Literal constant:

         (3, FALSE, id[nat])

• No zero- or one-tuples

• Tuples and functions are closely related:

         [[t_{1},. . . t_{n}] -> t] ≡ [t_{1},. . . t_{n} -> t]

         f((x,y)) ≡ f(x,y)

Records

• Type declaration:

         thing:  [# p:  nat, foo:  stack #]

• Dereferencing (Note: not thing.p):

         p(thing)

• Literal constant:

         (# p := 0, foo := emptystack #)

Function Updates/Overriding

• A way of defining a new function that has the same value as

another function except at specified points:

         foo WITH [(1) := 4, (z) := p+q]

• Semantics:

         f WITH [(x) := y](z) = IF x=z THEN y ELSE f(z) ENDIF

• Same construction applies to records:

         thing WITH [(p) := p(thing)+1]

Higher-Order

• Functions can take and return functions as values

(also tuples, records)

    injective? : pred[[dom -> rng]]
       = (LAMBDA (f:[dom->rng]):
           (FORALL (x,y:dom): (f(x) = f(y) => (x = y))))
    test: LEMMA injective?(suc)

• Quantification can range over functions:

     P: VAR [nat -> bool]
     simple_induction: LEMMA
       (FORALL P, m: P(0) AND (FORALL n: P(n) IMPLIES P(n+1))
          IMPLIES P(m))

Theory Assumptions

• Consider a theory that specifies sorting:

         sorting [T: TYPE, <=:  [T, T -> bool]]:  THEORY

• Where the idea is to sort sequences of the type T wrt. the ordering relation <=

• And suppose we instantiate with:

         IMPORTING sorting[nat, =[nat]]

• Clearly no good—we need to state semantic restrictions on the allowed actual parameters

• This is done in an ASSUMING clause (comes immediately after

  BEGIN)

• Inside the theory, formulas in the ASSUMING clause may be assumed as axioms; whenever instantiated, required to demonstrate that actual parameters satisfy those formulas

Subtypes

• Can define subtypes of existing types

• Either uninterpreted:

         magic numbers:  TYPE FROM nat

• Or associated with a predicate:

         posint:  TYPE = {n:nat | n > 0}

• If the predicate is p, this can be written as (p)

• Can provide a witness that subtype is not empty:

         posint:  TYPE = {n:nat | n > 0} CONTAINING 1

• Can declare constants, variables of the subtype, and use anywhere a type is required

• Can supply a term of a subtype where one of the supertype is expected

• And vice-versa if associated predicate satisfied in the context • System generates a proof obligation (TCC) in this case

pvscourse 25

Subtype Example

thing [m,n: nat] : THEORY
BEGIN
ASSUMING
  assump1: ASSUMPTION m < n
ENDASSUMING
x: VAR nat
posint: TYPE {x:nat | x>0}
diff: posint = n-m
END thing

TCC generated has form

   diff TCC1:  OBLIGATION n-m > 0

Can obviously be proved from module assumptions

PVS has a default strategy for attempting proofs of TCCs

All TCCs must be proved before specification considered verified

pvscourse 26

Division is Made a Total Function Using Subtypes

x, y: VAR number
nonzero_rational TYPE = {x: rational | x /= 0}
/: [rational, nonzero_rational -> rational]
eg: LEMMA x /= y IMPLIES (y - x)/(x - y) < 0
eg_TCC1: OBLIGATION
   (FORALL x, y: x /= y IMPLIES (x - y) /= 0)

Recursive Definitions

• Recursive definitions must be shown to “terminate”

• This is done by attaching a measure function to the declaration

• Measure function has same domain as function being declared, but range type nat

• Must show that value of measure function decreases across

recursive calls:

    factorial((a:nat)): RECURSIVE nat =
       IF a=0 THEN 1 ELSE a * factorial(a-1) ENDIF
      MEASURE id
    factorial_TCC2: OBLIGATION
      (FORALL (a: nat):
        NOT a = 0 IMPLIES id[nat](a - 1) < id[nat](a))

pvscourse 28

TCCs

• TCCs are generated in three circumstances:

∘ Nonemptiness of predicate subtypes ∘ Supertype to subtype coercions ∘ Recursive definitions

• TCCs are revealed by show-tccs and prettyprint-expanded

commands

Example TCCs

tcctest: THEORY
BEGIN
x,y: VAR int
pos: TYPE = {x:int | x > 0}
p: pos
square: (injective?[int, nat]) = (LAMBDA (x: int): x * x)
a: VAR nat
id(a): nat = a
factorial(a): RECURSIVE pos =
   IF a=0 THEN 1 ELSE a * factorial(a-1) ENDIF
  MEASURE id
END tcctest

Example TCCs (Continued 1)

% Existence TCC generated for pos
  % unproved
p_TCC1: OBLIGATION (EXISTS (x1: int): x1 > 0)
% Subtype TCC generated for x * x
  % unproved
square_TCC1: OBLIGATION (FORALL (x: int): x * x >= 0)
% Subtype TCC generated for (LAMBDA (x: int): x * x)
  % unproved
square_TCC2:
  OBLIGATION
    (FORALL (x1: int):
       injective?[int, nat]((LAMBDA (x: int): x * x)) AND x1 * x1 >= 0)

Example TCCs (Continued 2)

% Subtype TCC generated for 1
  % unproved
factorial_TCC1: OBLIGATION (FORALL a: a = 0 IMPLIES 1 > 0)
% Subtype TCC generated for a - 1
  % unproved
factorial_TCC2: OBLIGATION (FORALL a: NOT a = 0 IMPLIES a - 1 >= 0)
% Termination TCC generated for factorial
  % unproved
factorial_TCC3: OBLIGATION (FORALL a: NOT a = 0 IMPLIES id(a - 1) < id(a))
% Subtype TCC generated for a * factorial(a - 1)
  % unproved
factorial_TCC4:
  OBLIGATION (FORALL a, (v: [nat -> pos]):
                NOT a = 0 IMPLIES a * v(a - 1) > 0)

Abstract Datatypes

• stack[T : TYPE] : DATATYPE
    BEGIN
    empty: empty?
    push(top: T, pop: stack): nonempty?
    END stack

• empty and push are constructors—used to build elements of the type

• top and pop are accessors—used for accessing the components of an element

• empty? and nonempty? are recognizers—used to classify elements of type stack

Theory Generated by stack Datatype

% Generated from file stack.pvs
stack_adt[T: TYPE]: THEORY
BEGIN
stack: TYPE
empty?, nonempty?: [stack -> boolean]
empty: (empty?)
push: [T, stack -> (nonempty?)]
top: [(nonempty?) -> T]
pop: [(nonempty?) -> stack]
empty_extensionality: AXIOM
  (FORALL (empty?_var: (empty?)), (empty?_var2: (empty?)):
     empty?_var = empty?_var2)
push_extensionality: AXIOM
  (FORALL (nonempty?_var: (nonempty?)), (nonempty?_var2: (nonempty?)):
     top(nonempty?_var) = top(nonempty?_var2)
       AND pop(nonempty?_var) = pop(nonempty?_var2)
       IMPLIES nonempty?_var = nonempty?_var2)

Theory Generated by stack Datatype (continued 1)

push_eta: AXIOM
  (FORALL (nonempty?_var: (nonempty?)):
     push(top(nonempty?_var), pop(nonempty?_var)) = nonempty?_var)
top_push: AXIOM
  (FORALL (push1_var: T), (push2_var: stack):
     top(push(push1_var, push2_var)) = push1_var)
pop_push: AXIOM
  (FORALL (push1_var: T), (push2_var: stack):
     pop(push(push1_var, push2_var)) = push2_var)
stack_disjoint: AXIOM
  (FORALL (stack_var: stack):
     NOT (empty?(stack_var) AND nonempty?(stack_var)))
stack_inclusive: AXIOM
  (FORALL (stack_var: stack): empty?(stack_var) OR nonempty?(stack_var))
stack_induction: AXIOM
  (FORALL (p: [stack -> boolean]):
     p(empty)
       AND
       (FORALL (push1_var: T), (push2_var: stack):
          p(push2_var) IMPLIES p(push(push1_var, push2_var)))
       IMPLIES (FORALL (stack_var: stack): p(stack_var)))

Theory Generated by stack Datatype (continued 2)

stack_nat_rec((empty?_fun: nat), (nonempty?_fun: [T, nat -> nat])):
[stack -> nat] =
LAMBDA (stack_var: stack):
CASES stack_var OF
  empty: empty?_fun,
  push(push1_var, push2_var):
      nonempty?_fun(push1_var,
                    stack_nat_rec(empty?_fun,
                                  nonempty?_fun)(push2_var))
ENDCASES
stack_ordinal_rec((empty?_fun: ordinal),
          (nonempty?_fun: [T, ordinal -> ordinal])):
[stack -> ordinal] =
LAMBDA (stack_var: stack):
CASES stack_var OF
  empty: empty?_fun,
  push(push1_var, push2_var):
      nonempty?_fun(push1_var,
                    stack_ordinal_rec(empty?_fun,
                                      nonempty?_fun)(push2_var))
ENDCASES
END stack_adt

Second Theory Generated by stack Datatype (Parameterized)

stack_rec_mod[T: TYPE, range: TYPE]: THEORY
BEGIN
IMPORTING stack_adt[T]
stack_rec((empty?_fun: range), (nonempty?_fun: [T, range -> range])):
  [stack -> range] =
      LAMBDA (stack_var: stack):
        CASES stack_var OF
          empty: empty?_fun,
          push(push1_var, push2_var):
              nonempty?_fun(push1_var,
                            stack_rec(empty?_fun,
                                      nonempty?_fun)(push2_var))
        ENDCASES
END stack_rec_mod

Dependent Types

• Function, record, and tuple types may be dependent

• pfun: TYPE = [# dom: predicate[t1], pfn:[(dom)->t2] #]
• date: TYPE = [y,m:nat, {d:nat | d <= days(m,y)}]
• tmod: TYPE = [n,m:int -> {x:nat | x < m}]

Dependent Types Example: subp

partialfun: THEORY
BEGIN
i, j: VAR int
subp(i,(j|i>=j)): RECURSIVE int =
    (IF i=j THEN 0 ELSE subp(i,j+1)+1 ENDIF)
  MEASURE (LAMBDA i,(j|i>=j): i-j)
subp_fact: LEMMA i>=j IMPLIES subp(i,j) = (i-j)
END partialfun

                    subp TCCs

% unchecked
subp_TCC1: OBLIGATION (FORALL i, (j: int | i >= j): i - j >= 0)
% unchecked
subp_TCC2:
OBLIGATION (FORALL i, (j: int | i >= j): NOT i = j IMPLIES i >= j + 1)
% unchecked
subp_TCC3:
OBLIGATION
  (FORALL i, (j: int | i >= j): NOT i = j IMPLIES i - (j + 1) < i - j)

Dependent Stacks Example

newstacks[t: TYPE]: THEORY
EXPORTING ALL
BEGIN
i: VAR nat
stack: TYPE = [# size: nat, elements: ARRAY[{i | i < size} -> t] #]
u, s: VAR stack
x, y: VAR t
e: t
nonemptystack?(s): bool = (size(s) > 0)
empty: stack = (# size := 0, elements := (LAMBDA (j: {i | i < 0}): e) #)
push(x, s):
  (nonemptystack?)
    = (# size := size(s) + 1,
         elements := elements(s) WITH [(size(s)) := x] #)

Dependent Stacks Example (continued)

ns: VAR (nonemptystack?)
pop(ns):
  stack
    = (# size := size(ns) - 1,
         elements := (LAMBDA (j: {i | i < size(ns) - 1}): elements(ns)(j))
         #)
top(ns): t = (elements(ns)(size(ns) - 1))
pop_push: LEMMA pop(push(x, s)) = s
push_ext: LEMMA push(x, u) = push(y, s) IMPLIES (x = y) AND (u = s)
END newstacks

Dependent Stacks TCCs

% Subtype TCC generated for elements(s) WITH [(size(s)) := x]
push_TCC1:
  OBLIGATION
    (FORALL s, (x2: nat): x2 < size(s) + 1 IFF x2 < size(s) OR x2 = (size(s)))
% Subtype TCC generated for
    % (# size := size(s) + 1, elements := elements(s) WITH [(size(s)) := x] #)
push_TCC2:
  OBLIGATION
    (FORALL s, x:
       nonemptystack?((# size := size(s) + 1,
                         elements :=
                           elements(s) WITH [(size(s)) := x]
                         #)))
% Subtype TCC generated for size(ns) - 1
pop_TCC1: OBLIGATION (FORALL ns: size(ns) - 1 >= 0)
% Subtype TCC generated for j
pop_TCC2: OBLIGATION (FORALL ns, (j: i | i < size(ns) - 1): j < size(ns))
% Subtype TCC generated for size(ns) - 1
top_TCC1: OBLIGATION (FORALL ns: size(ns) - 1 >= 0 AND size(ns) - 1 < size(ns))

PVS Proof Checker

• Interactive—user makes all significant decisions, proof checker does the mundane work

• Has powerful decision procedures

• And conditional rewriting—can be made automatic

• Uses the language of PVS—no translation needed

Proofs

• Aim is to build a proof tree in which all of the leaves are true • Each node of the proof tree is a sequent consisting of

antecedent formulas and succedent formulas

• The meaning of a sequent is that the conjunction of the antecedents implies the disjunction of the succedents

• The proof checker is always focused at a leaf sequent of the tree—the current goal

• Proof checker commands either reduce current goal to true, or add new subgoal(s)—one of which becomes the current goal

Proof Checker Commands

• The PVS proof checker has commands for: ∘ Manipulating the proof tree—e.g., undo, postpone, fail ∘ Propositional reasoning—e.g., flatten, split, case ∘ Eliminating quantifiers—e.g., skolem!, quant ∘ Equality reasoning—e.g., rewrite, expand ∘ Applying the decision procedures—assert ∘ Performing inductions and extensionality arguments—e.g.,

  induct

∘ Combining commands to make strategies—e.g., try, then*

Propositional Rules

\overline{Γ, A ⊢ B, Δ} Ax  where A ≡ B

\frac{Γ, A ⊢ Δ  Γ ⊢ A, Δ}{Γ ⊢ Δ}  Cut

\frac{A, B, Γ ⊢ Δ}{A ∧ B, Γ ⊢ Δ} ∧ ⊢  \frac{Γ ⊢ A, Δ Γ ⊢ B, Δ}{Γ ⊢ A ∧ B, Δ}  ⊢ ∧

\frac{A, Γ ⊢ Δ B, Γ ⊢ Δ}{A ∨ B, Γ ⊢ Δ}  ∨ ⊢  \frac{Γ ⊢ A, B, Δ}{Γ ⊢ A ∨ B, Δ} ⊢ ∨

\frac{B, Γ ⊢ Δ Γ ⊢ A, Δ}{A ⊃ B, Γ ⊢ Δ}  ⊃ ⊢  \frac{Γ, A ⊢ B, Δ}{Γ ⊢ A ⊃ B, Δ} ⊢ ⊃

\frac{Γ ⊢ A, Δ}{Γ, ¬A ⊢ Δ} ¬ ⊢  \frac{Γ, A ⊢ Δ}{Γ ⊢ ¬A, Δ} ⊢ ¬

pvscourse 47

Equality and Quantifier Rules

\overline{Γ ⊢ a = b, Δ} Refl if a ≡ b  \frac{a = b, Γ[b] ⊢ Δ[b]}{a = b, Γ[a] ⊢ Δ[a]} Repl

\frac{Γ, A\{x ← t\} ⊢ Δ}{Γ, (∀x: A) ⊢ Δ} ∀ ⊢  \frac{Γ ⊢ A\{x ← a\}, Δ}{Γ ⊢ (∀x: A), Δ} ⊢ ∀

\frac{Γ, A\{x ← a\} ⊢ Δ}{Γ, (∃x: A) ⊢ Δ} ∃ ⊢  \frac{Γ ⊢ A\{x ← t\}, Δ}{Γ ⊢ (∃x: A), Δ} ⊢ ∃

pvscourse 48

Decision Procedures

• The decision procedures can be invoked by command

• Many commands use decision procedures for control (e.g. conditional rewrites)

• Procedure based on Shostak’s “combination of theories”

• Combines decision procedures for ground theories of: ∘ Equality ∘ Linear arithmetic over integers and reals ∘ Typed lambda calculus ∘ Arrays

Arithmetic Decision Procedures

• PVS proofs make heavy use of arithmetic decision procedures

• THEOREMs below are proved automatically

• CONJECTUREs are either false or unproved by decision procedures

  arithmetic : THEORY
  BEGIN
    x,y,v: VAR number
    arith: THEOREM
      x < 2*y AND y < 3*v IMPLIES 3*x < 18*v
    badarith: CONJECTURE
      x < 2*y AND y < 3*v IMPLIES 3*x < 17*v
    badarith2: CONJECTURE
      x<0 AND y<0 IMPLIES x*y>0

Arithmetic Decision Procedures (continued)

baddiv: CONJECTURE
  (x/y) > v IMPLIES x > (y*v)
gooddiv: CONJECTURE
  y/=0 AND (x/y) > v IMPLIES x > (y*v)
anotherdiv: THEOREM
  y /= 0 AND (x/y) > (v/y) IMPLIES ((x-v)/y) > 0
i, j, k: VAR int
intarith: THEOREM
  2*i < 5 AND i > 1 IMPLIES i = 2
badarith3: CONJECTURE
  2*x < 5 AND x > 1 IMPLIES x = 2
END arithmetic

Summary

• Language of PVS attempts to support conventional mathematical practice and notation within a framework that permits rigorous consistency-checking and effective deduction

• PVS proof checker combines powerful automation at the low-level, with straightforward user-guidance at the high-level

• PVS has been used to verify ∘ Byzantine agreement under a hybrid fault model ∘ Alternating bit protocol ∘ Constraints on simple real-time controller ∘ Equivalence of simple and pipelined microprocessor

architectures ∘ Microcode for simple microprocessor ∘ A version of the Schröder-Bernstein theorem

System and Documentation

• PVS is available by anonymous FTP from

    ftp.csl.sri.com in /pub/pvs/pvs-01.tar.Z

(Allegro lisp implementation for Sun SparcStations)

• PVS Documentation included:

∘ PVS Tutorial

∘ User Guide for the PVS Specification and Verification

System ∘ The PVS Specification Language ∘ The PVS Proof Checker: A Reference Manual

• (These are also available in /pub/pvs/pvs-doc.tar.Z)

• Reports (including work done with PVS) available in

  /pub/reports, get readme.txt for an index