Transcript CSE 8389

CSE 8389
Theorem Proving
Peter-Michael Seidel
CSE 8389 Theorem Proving - Seidel
Spring 2005
1
Syntax vs Semantics
Syntax
– a.k.a. “formation rules”; “grammar”; …
– prescribes what a well-formed formula is (syntactically)
Semantics
– the “meaning” of well-formed formulas
– defined via a mapping called interpretation
CSE 8389 Theorem Proving - Seidel
Spring 2005
2
Propositional Logic: Syntax
propositional logic
logic> (or "propositional calculus") A system of symbolic logic using symbols to stand
for whole propositions and logical connectives. Propositional logic only considers
whether a proposition is true or false. In contrast to predicate logic, it does not consider
the internal structure of propositions. http://wombat.doc.ic.ac.uk/foldoc/foldoc.cgi?propositional+logic
<
Logical symbols:
– conjunction: , disjunction: , negation: ,
– implication: , equivalence: , parentheses:  
Non-logical symbols:
– propositional variables p, q, r, ...
– signature: set of propositional variables  = {p, q, r, ...}
Formation rules for well-formed formulas (wff)
– an atomic formula (propositional variable) is a formula
– if F, G are formulas, so are:
•
FG, F  G,  F, FG , FG,  F 
CSE 8389 Theorem Proving - Seidel
Spring 2005
3
Propositional Logic: Semantics
Propositions can be assigned a truth-value:
– either true or false (classical 2-valued logic: tertium non datur)
– other propositional logics exist: 3-valued, 4-valued, temporal, … (modal
logics), …, fuzzy logic
An interpretation I over a signature  is a mapping
– I:   {true, false} , associating a truth value to every propositional
variable
Truth tables describe how to extend I from atomic to composite
formulas (Boolean Algebra):
– FG, F  G,  F, FG , FG
CSE 8389 Theorem Proving - Seidel
Spring 2005
4
Boolean Algebra, Truth Tables
CSE 8389 Theorem Proving - Seidel
http://wombat.doc.ic.ac.uk/foldoc/foldoc.cgi?two-valued+logic
Spring 2005
5
Different Logical Bases
Often:
– ,  , 
Alternatively:
–
–
–
–
–
–
, 
, 
NAND
NOR
XOR
ite(A,B,C)
if A then B else C ?
CSE 8389 Theorem Proving - Seidel
Spring 2005
6
Reasoning in Propositional Logic
A formula F is …
–
–
–
valid if it is true for all interpretations I
satisfiable if it is true for some interpretation I
unsatisfiable if it is true for no interpretation I
Try these:
1.
2.
3.
4.
5.
6.
pq
p  p
p  p
pp
p  p
pp
CSE 8389 Theorem Proving - Seidel
Spring 2005
7
Reasoning in Propositional Logic
Def. “models” relationship “|=”:
–
–
If a formula F evaluates to true for an interpretation I then I is called
a model of F; written I |= F
I is a model of {F1,…, Fk}, written I |= {F1,…, Fk},if I is a model of each Fj
Automated deduction setting:
–
–
–
–
Show that A1,,…, An (axioms) imply T (theorem), that is, every model of
the axioms is also a model of the theorem:
That is: if I |= {A1,,…, An } then I |= T
Short: {A1,,…, An } |= T
Often: Show that A1  …  An  T is unsatisfiable
For Automation a procedure / reasoning algorithm is needed:
–
Predicate Calculus (in fact calculi: resolution, tableaux, …)
CSE 8389 Theorem Proving - Seidel
Spring 2005
8
Example
{p, p  q } |= q
–
–
–
–
Truth table
Resolution
Tableaux
Reasoning with BDDs
CSE 8389 Theorem Proving - Seidel
Spring 2005
9
Example: Reasoning with Binary Decision Trees
(see also: Binary Decision Diagrams, or BDDs)
A
… B
A
A
if-false
A
if-true
0
1
false
true
0
1
B
0
A
0
1
0
true
false
B
0
CSE 8389 Theorem Proving - Seidel
0
1
AB
A
if-true
1
B
0
…B
A
if-false
AB
A
1
1
B
0
Spring 2005
1
1
10
Syntax of First-Order Logic (FO)
Logical symbols:
– , , , , ,  ,  (“for all”),  (“exists”), ...
Non-logical symbols: A FO signature  consists of
– constant symbols: a,b,c, ...
– function symbols: f, g, ...
– predicate (relation) symbols: p,q,r, ....
function and predicate symbols have an associated arity;
– we can write, e.g., p/3, f/2 to denote the ternary predicate p and the
function f with two arguments
First-order variables: x, y, ...
Formation rules for terms:
– constants and variables are terms
– if t1,…,tk are terms and f is a k-ary function symbols then f(t1,...,tk) is a
term
CSE 8389 Theorem Proving - Seidel
Spring 2005
11
Syntax of First-Order Logic (FO)
Formation rules for formulas:
– if t1,…, tk are terms and p/k is a predicate symbol (of arity k) then p(t1,
…, tk) is an atomic formula (short: atom)
• all variable occurrences in p(t1, …, tk) are free
– if F,G are formulas and x is a variable, then the following are formulas:
– FG, F  G,  F, FG , FG,  F ,
– x: F (“for all x: F(x,...) is true”)
– x: F (“there exists x such that F(x,...) is true”)
– the occurrences of a variable x within the scope of a quantifier are
called bound occurrences.
CSE 8389 Theorem Proving - Seidel
Spring 2005
12
Examples
x man(x)  person(x).
man(bill).
child(marriage(bill,hillary),chelsea).
Variable: x
Constants (0-ary function symbols): bill/0, hillary/0, chelsea/0
Function symbols: marriage/2
Predicate symbols: man/1, person/1, child/2
CSE 8389 Theorem Proving - Seidel
Spring 2005
13
Semantics of Predicate Logic
Let D be a non-empty domain (a.k.a. universe of discourse). A structure is a
pair I = (D,I), with an interpretation I that maps ...
– each constant symbols c to an element I(c) D
– each predicate symbol p/k to a k-ary relation I(p)  Dk,
– each function symbol f/k to a k-ary function I(f): DkD
Let I be a structure,  : Vars  D a variable assignment. A valuation valI,
maps Term to D and Fml to {true, false}
–
–
–
–
–
–
–
–
valI, (x) =  (x)
; for x  Vars
valI, (f(t1,...,tk)) = I(f)( valI, (t1),..., valI, (tk) )
; for f(t1,...,tk)  Term
valI, (p(t1,...,tk)) = I(p)( valI, (t1),..., valI, (tk) )
; for p(t1,...,tk)  At
valI, (F  G) = valI, (F) and valI, (G) are true
; for F,G Fml
valI, (F  G) = valI, (F) or valI, (G) is true
; for F,G Fml
valI, ( F) = true (false) if valI, (F) is false (true) ; for FFml
valI, ( x F) = valI,[x/t] (F) is true for some t  D
; for FFml
valI, ( x F) = valI,[x/t] (F) is true for all t  D
; for FFml
CSE 8389 Theorem Proving - Seidel
Spring 2005
14
Example
Formula F = x man(x)  person(x).
Domain D = {b, h, c, d, e}
Let’s pick an interpretation I:
I(bill) = b, I(hillary) = h, I(chelsea) = c
I(person) = {b, h, c}
I(man) = {b}
Under this I, the formula F evaluates to true.
If we choose I’ like I but I’(man) = {b,d}, then F evaluates to false
Thus, I is a model of F, while I’ is not:
– I |= F
I’ |=/= F
CSE 8389 Theorem Proving - Seidel
Spring 2005
15
FO Semantics (cont’d)
F entails G (G is a logical consequence of F) if every model of F is also a
model of G:
F |= G
F is consistent or satisfiable if it has at least one model
F is valid or a tautology if every interpretation of F is a model
Proof Theory:
Let F,G, ... be FO sentences (no free variables).
Then the following are equivalent:
F_1, ..., F_k |= G
F_1  ...  F_k  G is valid
F_1  ...  F_k   G is unsatisfiable (inconsistent)
CSE 8389 Theorem Proving - Seidel
Spring 2005
16
Querying vs. Reasoning
Querying:
– given a DB instance I (= logic interpretation), evaluate a query expression
(e.g. SQL, FO formula, Prolog program, ...)
– boolean query: check if I |= 
(i.e., if I is a model of )
– (ternary) query: { (X, Y, Z) | I |=  (X,Y,Z) }
=> check happyFathers in a given database
Reasoning:
– check if I |=  implies I |=  for all databases I,
– i.e., if  => 
– undecidable for FO, F-logic, etc.
– Descriptions Logics are decidable fragments
 concept subsumption, concept hierarchy, classification
 semantic tableaux, resolution, specialized algorithms
CSE 8389 Theorem Proving - Seidel
Spring 2005
17
Reasoning Example
(1) p(0)
(2) x p(x)  p(s(x))
(3) p(s(s(0))).
We want to show that (1) & ... & (2) implies (3)
Approach: assume negation of (3) and show that it leads to a
contradiction with {(1), (2)}
– Question: Why is this sound?
CSE 8389 Theorem Proving - Seidel
Spring 2005
18
Limitations
Drawbacks of methods based on FOL/Predicate Logic:
• only small and medium size circuits can be verified
• most abstract representation view is gate level
• Complex circuits are hierarchically designed,
but verification methods are not able to benefit from this
to reduce the verification complexity
Caused by limited expressiveness of underlying logic –
one can not even argue about simple natural numbers
a
Natural numbers useful to argue about
discrete time
parameterized circuits:
FORALL n>0, FORALL a,b,c in Bn: <a> + <b> = <c>
b
ADD(n)
c
More expressive logic also needed to allow abstract descriptions (types)
CSE 8389 Theorem Proving - Seidel
Spring 2005
19
Sentences in FirstOrder Logic
An atomic sentence is simply a predicate applied to a set of terms.
– Owns(John,Car1)
– Sold(John,Car1,Fred)
Semantics is True or False depending on the interpretation, i.e. is the
predicate true of these arguments.
The standard propositional connectives ( ) can be used to
construct complex sentences:
– Owns(John,Car1)  Owns(Fred, Car1)
– Sold(John,Car1,Fred)  ¬Owns(John, Car1)
Semantics same as in propositional logic.
CSE 8389 Theorem Proving - Seidel
Spring 2005
20
Review: Quantifiers
Allow statements about entire collections of objects
Universal quantifier: x
– Asserts that a sentence is true for all values of variable x
•
•
•
x Loves(x, FOPC)
x Whale(x)  Mammal(x)
x y Dog(y)  Loves(x,y))  z Cat(z)  Hates(x,z))
Existential quantifier: 
– Asserts that a sentence is true for at least one value of a variable x
•
•
x Loves(x, FOPC)
x(Cat(x)  Color(x,Black)  Owns(Mary,x))
•
x(y Dog(y)  Loves(x,y))  (z Cat(z)  Hates(x,z))
CSE 8389 Theorem Proving - Seidel
Spring 2005
21
Review: Use of Quantifiers
Universal quantification naturally uses implication:
–
x Whale(x)  Mammal(x)
• Says that everything in the universe is both a whale and a mammal.
Existential quantification naturally uses conjunction:
–
x Owns(Mary,x)  Cat(x)
• Says either there is something in the universe that Mary does not own or
there exists a cat in the universe.
–
x Owns(Mary,x)  Cat(x)
• Says all Mary owns is cats (i.e. everthing Mary owns is a cat). Also true if
Mary owns nothing.
–
x Cat(x)  Owns(Mary,x)
• Says that Mary owns all the cats in the universe. Also true if there are
no cats in the universe.
CSE 8389 Theorem Proving - Seidel
Spring 2005
22
Nesting Quantifiers
The order of quantifiers of the same type doesn't matter:
–
–
xy(Parent(x,y)  Male(y)  Son(y,x))
xy(Loves(x,y)  Loves(y,x))
The order of mixed quantifiers does matter:
–
xy(Loves(x,y))
• Says everybody loves somebody, i.e. everyone has someone whom they love.
–
yx(Loves(x,y))
• Says there is someone who is loved by everyone in the universe.
–
yx(Loves(x,y))
• Says everyone has someone who loves them.
–
xy(Loves(x,y))
• Says there is someone who loves everyone in the universe.
CSE 8389 Theorem Proving - Seidel
Spring 2005
23
Variable Scope
The scope of a variable is the sentence to which the quantifier
syntactically applies.
As in a block structured programming language, a variable in a
logical expression refers to the closest quantifier within
whose scope it appears.
–
x (Cat(x)  x(Black (x)))
• The x in Black(x) is universally quantified
• Says cats exist and everything is black
In a wellformed formula (wff) all variables should be properly
introduced:
–
xP(y) not wellformed
A ground expression contains no variables.
CSE 8389 Theorem Proving - Seidel
Spring 2005
24
Relations Between Quantifiers
Universal and existential quantification are logically
related to each other:
– x ¬Love(x,Saddam)  ¬x Loves(x,Saddam)
– x Love(x,PrincessDi)  ¬x ¬Loves(x,PrincessDi)
General Identities
–
–
–
–
–
–
x ¬P  ¬x P
¬x P  x ¬P
x P  ¬x ¬P
x P  ¬x ¬P
x P(x)  Q(x)  x P(x)  x Q(x)
x P(x)  Q(x)  x P(x)  x Q(x)
CSE 8389 Theorem Proving - Seidel
Spring 2005
25
Equality
Can include equality as a primitive predicate in the logic, or require it to be
introduced and axiomatized as the identity relation.
Useful in representing certain types of knowledge:
– xy(Owns(Mary, x)  Cat(x)  Owns(Mary,y)  Cat(y)
–  ¬(x=y))
– Mary owns two cats. Inequality needed to ensure x and y are distinct.
– x y married(x, y) z(married(x,z)  y=z)
– Everyone is married to exactly one person. Second conjunct is needed to
guarantee there is only one unique spouse.
CSE 8389 Theorem Proving - Seidel
Spring 2005
26
HigherOrder Logic
FOPC is called firstorder because it allows quantifiers to range over
objects (terms) but not properties, relations, or functions applied to
those objects.
Secondorder logic allows quantifiers to range over predicates and
functions as well:
–
 x  y [ (x=y)  ( p p(x)  p(y)) ]
• Says that two objects are equal if and only if they have exactly the same
properties.
–
 f  g [ (f=g)  ( x f(x) = g(x)) ]
• Says that two functions are equal if and only if they have the same value for all
possible arguments.
Thirdorder would allow quantifying over predicates of predicates, etc.
We will consider Higher-Order Logic = FOL & Second-order Logic & …
allows to argue about infinite sets, use induction
CSE 8389 Theorem Proving - Seidel
Spring 2005
27
Problems with Higher order Logic
Higher-Order Logic is Undecidible
Theorem Provers based on HOL have to be interactive.
(Informal Version’s of) Russel’s Paradox
• In a certain town in Spain, there lives an excellent barber who shaves
all the men who do not shave themselves. Who shaves the barber?
• Divide all adjectives into two groups: the group of adjectives which
describe themselves and the group of adjectives which do not. Into
which group does the adjective indescribable go?
• I am a liar.
Russel’s Paradox can be resolved by introducing typed Higher-order logic
CSE 8389 Theorem Proving - Seidel
Spring 2005
28
What is PVS?
PVS = Prototype Verification System
Formal specification language
Model checker
Theorem prover
Documentation tools, etc.
CSE 8389 Theorem Proving - Seidel
Spring 2005
29
Applications
Academic and industrial applications
– Hardware verification
(e.g. VAMP – Verified Architecture Microprocessor)
– Protocol verification
– Verification of Javacard applets
– Formal Mathematics
– Safety-critical systems
– … (see http://pvs.csl.sri.com/users.html)
CSE 8389 Theorem Proving - Seidel
Spring 2005
30
The PVS Language
There are two languages
1.
The language to write definitions and theorems
(“definition language“)
2. 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
CSE 8389 Theorem Proving - Seidel
Spring 2005
31
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
CSE 8389 Theorem Proving - Seidel
Spring 2005
32
The PVS Definition Language
class_theory: THEORY BEGIN
my_type: NONEMPTY_TYPE
constant1, constant2: my_type
Type
Declarations
f1: THEOREM
FORALL (a, b: integer): a+b=b+a
f2: AXIOM
constant1=constant2
Expressions
END class_theory
CSE 8389 Theorem Proving - Seidel
Spring 2005
33 A
The PVS Definition Language
class_theory: THEORY BEGIN
my_type: NONEMPTY_TYPE
constant1, constant2: my_type
f1: THEOREM
FORALL (a, b: integer): a+b=b+a
f2: AXIOM
constant1=constant2
Formulae
END class_theory
CSE 8389 Theorem Proving - Seidel
Spring 2005
34 A
The PVS Definition Language
class_theory: THEORY BEGIN
my_type: NONEMPTY_TYPE
constant1, constant2: my_type
f1: THEOREM
FORALL (a, b: integer): a+b=b+a
Declarations
f2: AXIOM
constant1=constant2
END class_theory
CSE 8389 Theorem Proving - Seidel
Spring 2005
35
Axioms vs. Theorems
Axioms are assumed to be true
Dangerous!
Avoid axioms, use constant declarations instead:
class_theory: THEORY BEGIN
class_theory: THEORY BEGIN
c: integer
c: integer = 3
c: AXIOM c=3
END class_theory
END class_theory
Left hand side is conservative
CSE 8389 Theorem Proving - Seidel
Spring 2005
36
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}
CSE 8389 Theorem Proving - Seidel
Spring 2005
37
Types PVS comes with
boolean
–
FALSE, TRUE
Number types
–
real, rational, integer, natural
string
Ordinals
CSE 8389 Theorem Proving - Seidel
Spring 2005
38
Type Expressions
Function Types
[ t1,…,tn -> t ]
Alternative Syntax:
FUNCTION[ t1,…,tn -> t ]
ARRAY[ t1,…,tn -> t ]
Note that ti and t may be function types as well!
CSE 8389 Theorem Proving - Seidel
Spring 2005
39
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
CSE 8389 Theorem Proving - Seidel
Spring 2005
40
Expressions
Function Applications
–
–
f(x)
Tons of Syntactic variants exist to support intuition, don’t be
confused
Binary operator symbols
y * z is the same as *(y, z)
CSE 8389 Theorem Proving - Seidel
Spring 2005
41
Expressions
Functions PVS comes with
–
–
–
Boolean
AND &, OR, IMPLIES =>,
WHEN, IFF <=>
IF c THEN a ELSE b
IF: [boolean, T, T -> T]
Numeric operators
+, -, *, /, ^, <, <=, >, >=
CSE 8389 Theorem Proving - Seidel
Spring 2005
42
Expressions
Binding Expressions
–
Quantifiers
EXISTS (x: T): p(x)
FORALL (y: T): q(y)
CSE 8389 Theorem Proving - Seidel
Spring 2005
43
Expressions
Binding Expressions
–
Lambda: unnamed functions
LAMBDA (x: int): x+1
Type of that: [ int -> int ]
class_theory: THEORY
BEGIN
f(x: int): int = x+1
END class_theory
CSE 8389 Theorem Proving - Seidel
class_theory: THEORY
BEGIN
f: [int->int] =
LAMBDA (x: int): x+1
END class_theory
Spring 2005
44 A
Recursion
Lambda cannot be used for recursion
Only named functions allow recursion
No mutual recursion
factorial(x: nat): RECURSIVE nat =
IF x=0 THEN
1
ELSE
factorial(x-1)*x
ENDIF
MEASURE (LAMBDA (x: nat): x)
Used to prove that the
function is total
CSE 8389 Theorem Proving - Seidel
Spring 2005
45 A
Expressions
LET Expressions
LET i:T=e1 IN e2
–
Useful for avoiding redundancy if e1 is used many times in e2
–
Example
LET x=2 IN x*y
is
(LAMBDA x: x*y)(2)
CSE 8389 Theorem Proving - Seidel
Spring 2005
46
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
CSE 8389 Theorem Proving - Seidel
Spring 2005
47
Expressions
LET and WITH useful for some sequential program constructs!
int f(int i) {
int a[10]={ 0, … };
...
a[i]=5;
...
return a[0];
}
CSE 8389 Theorem Proving - Seidel
f(i: int):int=
LET a1=LAMBDA (x: below(10)): 0 IN
...
LET a2=a1 WITH [(i):=5] IN
...
aj(0)
Spring 2005
48
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
CSE 8389 Theorem Proving - Seidel
Spring 2005
49
Some Additional Syntax
Tuple types
Tuple expressions
[ t1,…,tn ]
( e1,…,en )
Comes with projections
PROJ_1, PROJ_2, ..., PROJ_n
CSE 8389 Theorem Proving - Seidel
Spring 2005
50
Example
stacks1: THEORY BEGIN
stack: TYPE = [int, ARRAY[int->int]]
empty: stack = (0, (LAMBDA (j: int): 0))
size(s: stack):int = PROJ_1(s)
elements(s: stack):ARRAY[int->int] = PROJ_2(s)
push(x: int, s:stack): stack =
(size(s)+1, elements(s)How
WITH
[(size(s)):=x])
about
a “struct”?
pop(s:stack): stack = (size(s)-1, elements(s))
END stacks1
CSE 8389 Theorem Proving - Seidel
Spring 2005
51 A
Some Additional Syntax
Record types
Record expressions
Comes with projections
Or:
[# a1:t1,…,an:tn #]
(# a1:=e1,…,an:=en #)
a1, a2, ..., an
e`ai
CSE 8389 Theorem Proving - Seidel
Spring 2005
52
Example
stacks2: THEORY BEGIN
stack: TYPE = [# size: int, elements: ARRAY[int->int] #]
empty: stack = (# size:=0, elements:=(LAMBDA (j: int): 0) #)
push(x: int, s:stack): stack =
(# size:=s`size+1,
elements:=s`elements WITH [(s`size):=x] #)
pop(s:stack): stack =
(# size:=s`size-1,
elements:=s`elements #)
END stacks2
What about the
empty stack?
CSE 8389 Theorem Proving - Seidel
Spring 2005
53 A
Subtypes
{ x: T | p(x)}
p must be of type [ T -> boolean ]
Alternative syntax:
(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
CSE 8389 Theorem Proving - Seidel
Spring 2005
54
Subtypes
Subtypes in binding expressions
–
–
Forall, exists: forall (i: int | i>10): …
Lambda:
class_theory: THEORY
BEGIN
f(x: int | x/=0): real =
1/x
END class_theory
CSE 8389 Theorem Proving - Seidel
class_theory: THEORY
BEGIN
f: [ {x: int | x/=0 }->real] =
LAMBDA (x: int | x/=0): 1/x
END class_theory
Spring 2005
55
Example
stacks3: THEORY BEGIN
stack: TYPE = [# size: nat, elements: ARRAY[nat->int] #]
empty: stack = (# size:=0, elements:=(LAMBDA (j: nat): 0) #)
push(x: int, s:stack): { s: stack | s`size>=1 } =
(# size:=s`size+1,
elements:=s`elements WITH [(s`size):=x] #)
pop(s:stack | s`size>=1): stack =
(# size:=s`size-1,
elements:=s`elements #)
END stacks3
Properties?
CSE 8389 Theorem Proving - Seidel
Spring 2005
56 A
Example
stacks3: THEORY BEGIN
stack: TYPE = [# size: nat, elements: ARRAY[nat->int] #]
empty: stack = (# size:=0, elements:=(LAMBDA (j: nat): 0) #)
push(x: int, s:stack): { s: stack | s`size>=1 } =
(# size:=s`size+1,
elements:=s`elements WITH [(s`size):=x] #)
pop(s:stack | s`size>=1): stack =
(# size:=s`size-1,
elements:=s`elements #)
Does this work?
push_pop: THEOREM
FORALL (s: stack, x: int): pop(push(x, s))=s
END stacks3
CSE 8389 Theorem Proving - Seidel
Spring 2005
57 A
Example
stacks4: THEORY BEGIN
stack: TYPE = [# size: nat, elements: ARRAY[{i:nat|i<size}->int] #]
empty: stack = (# size:=0, elements:=(LAMBDA (j:nat| FALSE): 0) #)
push(x: int, s:stack): { s: stack | s`size>=1 } =
(# size:=s`size+1,
elements:=LAMBDA (j: below(s`size+1)):
IF j<s`size THEN s`elements(j) ELSE x ENDIF #)
pop(s:stack | s`size>=1): stack =
(# size:=s`size-1,
elements:=LAMBDA (j:nat|j<s`size-1): s`elements(j) #)
push_pop: THEOREM
FORALL (s: stack, x: int): pop(push(x, s))=s
END stacks4
CSE 8389 Theorem Proving - Seidel
Spring 2005
58
Example
stacks4: THEORY BEGIN
stack: TYPE = [# size: nat, elements: ARRAY[{i:nat|i<size}->int] #]
empty: stack = (# size:=0, elements:=(LAMBDA (j:nat| FALSE): 0) #)
push(x: int, s:stack): { s: stack | s`size>=1 } =
(# size:=s`size+1,
elements:=LAMBDA (j: below(s`size+1)):
IF j<s`size THEN s`elements(j) ELSE x ENDIF #)
What about the
pop(s:stack | s`size>=1): stack =
stacks of other
(# size:=s`size-1,
types?
elements:=LAMBDA (j:nat|j<s`size-1): s`elements(j)
#)
END stacks4
CSE 8389 Theorem Proving - Seidel
Spring 2005
59 A
Example
stacks4: THEORY BEGIN
stack: TYPE = [# size: nat, elements: ARRAY[{i:nat|i<size}->int] #]
empty: stack = (# size:=0, elements:=(LAMBDA (j:nat| FALSE): 0) #)
push(x: int, s:stack): { s: stack | s`size>=1 } =
(# size:=s`size+1,
elements:=LAMBDA (j: below(s`size+1)):
IF j<s`size THEN s`elements(j) ELSE x ENDIF #)
pop(s:stack | s`size>=1): stack =
(# size:=s`size-1,
elements:=LAMBDA (j:nat|j<s`size-1): s`elements(j) #)
END stacks4
CSE 8389 Theorem Proving - Seidel
Spring 2005
60
Theory Parameters
Idea: do something like a C++ template
template <class T1,
class T2, ...>
class stack
{
...
};
CSE 8389 Theorem Proving - Seidel
theory[T1: TYPE,
T2: TYPE, ...]:
THEORY BEGIN
...
END theory
Spring 2005
61 A
Theory Parameters
Idea: do something like a C++ template
template <class T1,
class T2, ...>
class stack
{
...
f(e: T1):bool;
...
};
theory[T1: TYPE,
T2: TYPE, ...]:
THEORY BEGIN
...
f(e: T1):bool;
...
END theory
CSE 8389 Theorem Proving - Seidel
Spring 2005
62
Example
stacks4[T: NONEMPTY_TYPE]: THEORY BEGIN
stack: TYPE = [# size: nat, elements: ARRAY[{i:nat|i<size}->T] #]
e: T
empty: stack = (# size:=0, elements:=(LAMBDA (j:nat| FALSE): e) #)
push(x: T, s:stack): { s: stack | s`size>=1 } =
(# size:=s`size+1,
elements:=LAMBDA (j: below(s`size+1)):
IF j<s`size THEN s`elements(j) ELSE x ENDIF #)
pop(s:stack | s`size>=1): stack =
(# size:=s`size-1,
elements:=LAMBDA (j:nat|j<s`size-1): s`elements(j) #)
END stacks4
CSE 8389 Theorem Proving - Seidel
Spring 2005
63
Example
use_stack: THEORY BEGIN
my_type: TYPE = [ posint, posint ]
IMPORTING stacks5;
s: stack[my_type];
x: my_type = (1, 2);
d: stack[my_type] = push(x , s);
END use_stack
CSE 8389 Theorem Proving - Seidel
Spring 2005
64
Useful Parameterized Theories
PVS comes with several useful parameterized theories
–
–
–
–
–
Sets over elements of type T
subsets, union, complement, power set,
finite sets, …
Infinite Sequences
Finite Sequences
Lists
Bit vectors
CSE 8389 Theorem Proving - Seidel
Spring 2005
65 A
Bit Vectors
Bit Vectors are defined using an ARRAY type
bv[N: nat]: THEORY
BEGIN
bvec : TYPE = [below(N) -> bit]
0, …, N-1
CSE 8389 Theorem Proving - Seidel
Spring 2005
same as
boolean
66 A
Bit Vectors
Extract a bit: bv^(i) i  { 0, … , N-1 }
Vector extraction: bv^(m,n) n≤m<N
bN: fill(b)
Concatenation: bv1 o bv2
Bitwise: bv1 OR bv2
Conversion to natural numbers: bv2nat(bv)
Conversion from natural numbers: nat2bv(nat)
CSE 8389 Theorem Proving - Seidel
Spring 2005
67
Bit Vector Arithmetic
Requires
IMPORTING bitvectors@bv_arith_nat
*, +, -, <=, >=, <, >
Many other useful theories
Look in pvs/lib/bitvectors
CSE 8389 Theorem Proving - Seidel
Spring 2005
68
Bit Vectors
Example:
bv_ex: THEORY BEGIN
x: VAR bvec[32]
zero_lemma: LEMMA bv2nat(x)=0 IFF x=fill(false)
END bv_ex
How many
bits?
CSE 8389 Theorem Proving - Seidel
Spring 2005
69 A
Bit Vectors
Example:
bv_ex: THEORY BEGIN
x: VAR bvec[32]
zero_lemma: LEMMA bv2nat[32](x)=0 IFF x=fill[32](false)
END bv_ex
CSE 8389 Theorem Proving - Seidel
Spring 2005
70
Modeling Combinational Hardware with PVS
Idea: Model combinational circuits using functions on bit
vectors
f(A, B, reset: bit):bit=
IF reset THEN
FALSE
ELSE
(NOT A) OR B
ENDIF
Translation from/to Verilog, VHDL, etc. easy
CSE 8389 Theorem Proving - Seidel
Spring 2005
71 A
Parameterized Circuits
Binary tree for 8 inputs
CSE 8389 Theorem Proving - Seidel
Parameterized for 2k inputs
Spring 2005
72 A
Modeling Hardware with PVS
btree[T: TYPE, K: posnat, o: [T,T->T]]: THEORY BEGIN
btree(k: nat, l:[below(exp2(k))->T]):
RECURSIVE T =
IF k=0 THEN
l(0)
ELSE
btree(k-1, LAMBDA (i: below(exp2(k-1))): l(i)) o
btree(k-1, LAMBDA (i: below(exp2(k-1))): l(i+exp2(k-1)))
ENDIF MEASURE k
btree(l:[below(exp2(K))->T]):T=btree(K, l)
END btree
Property?
CSE 8389 Theorem Proving - Seidel
Spring 2005
73 A
Modeling Hardware with PVS
btree[T: TYPE, K: posnat, o: [T,T->T]]: THEORY BEGIN
...
btree_correct: THEOREM
btree(l) = l(0) o l(1) o ... o l(exp(K)-1)
END btree
Dot dot dot?
CSE 8389 Theorem Proving - Seidel
Spring 2005
74 A
Modeling Hardware with PVS
btree[T: TYPE, K: posnat, o: [T,T->T]]: THEORY BEGIN
...
btree_correct: THEOREM
btree(l) = l(0) o l(1) o ... o l(exp(K)-1)
seq(i: nat, l:[upto(i)->T]): RECURSIVE T =
IF i=0 THEN
l(0)
ELSE
seq (i-1, LAMBDA (j: below(i)): l(j)) o l(i)
ENDIF
MEASURE i
Btree_correct: THEOREM
btree(l) = seq(exp(K)-1, l)
END btree
CSE 8389 Theorem Proving - Seidel
Spring 2005
Can
Whatyou
is
prove
missing?
this?
75 A
Modeling Hardware with PVS
btree[T: TYPE, K: posnat, o: [T,T->T]]: THEORY BEGIN
ASSUMING
fassoc: ASSUMPTION associative?(o)
ENDASSUMING
This is NOT
like an axiom!
...
END btree
zerotester_imp(op): bit =
NOT btree[bit, K, OR](op)
PVS will make you prove
here that OR is associative
CSE 8389 Theorem Proving - Seidel
Spring 2005
76 A
Arithmetic Circuits
a,b,cin : VAR bit
oba_sum(a,b,cin): bit =
(a XOR b XOR cin)
Wait a second!
bit =
Youoba_cout(a,b,cin):
are
adding
bits
here!
((a AND b) OR
One Bit Adder (oba)
(a AND cin) OR
(b AND cin))
Property?
oba_correct: LEMMA
a + b + cin = 2 * oba_cout(a,b,cin) + oba_sum(a,b,cin)
CSE 8389 Theorem Proving - Seidel
Spring 2005
77 A
Conversions
oba_correct: LEMMA
a + b + cin = 2 * oba_cout(a,b,cin) + oba_sum(a,b,cin)
There is no addition on bits (or boolean)!
bit : TYPE = bool
nbit : TYPE = below(2)
b2n(b:bool): nbit = IF b THEN 1 ELSE 0 ENDIF
CONVERSION b2n
below(2) is a subtype of the integer type,
and we have addition for that.
CSE 8389 Theorem Proving - Seidel
Spring 2005
78 A
Arithmetic Circuits
Carry Chain Adder
CSE 8389 Theorem Proving - Seidel
Spring 2005
79
Arithmetic Circuits
cout(n,a,b,a_cin): RECURSIVE bit =
IF n=0 THEN
oba_cout(a(0),b(0),a_cin)
ELSE
oba_cout(a(n),b(n),
cout(n-1,a,b,a_cin))
ENDIF MEASURE n
bv_adder(a,b,a_cin): bvec[N] =
LAMBDA (i:below(N)):
IF i=0 THEN
oba_sum(a(0),b(0),a_cin)
ELSE
oba_sum(x(i),y(i),
cout(i-1,x,y,a_cin))
ENDIF
CSE 8389 Theorem Proving - Seidel
Spring 2005
80 A
Arithmetic Circuits
bv_adder(a,b,a_cin): bvec[N] =
LAMBDA (i:below(N)):
IF i=0 THEN
oba_sum(a(0),b(0),a_cin)
ELSE
oba_sum(x(i),y(i),
cout(i-1,x,y,a_cin))
ENDIF
adder_correct: THEOREM
exp2(N)*cout(N-1,a,b,a_cin)+bv2nat(bv_adder(a,b,a_cin))=
bv2nat(a) + bv2nat(b) + a_cin
adder_is_add: THEOREM
bv_adder(a,b,FALSE) = a + b
CSE 8389 Theorem Proving - Seidel
Spring 2005
81 A
PVS Workflow
System
PROOFS
PVS File
Properties
of system
Proof construction
 Conversion

(Program, circuit, protocol…)
and property.
Interaction with the theorem
prover
Can be automated or done
manually
CSE 8389 Theorem Proving - Seidel
Spring 2005
82 A
PVS Workflow
System
PROOFS
PVS File
Properties
of system
Proof construction
 Conversion

(Program, circuit, protocol…)
and property.
Interaction with the theorem
prover
Can be automated or done
manually
CSE 8389 Theorem Proving - Seidel
Spring 2005
83 A
The PVS Language
There are two languages
1.
The language to write definitions and theorems
(“definition language“)
2. 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
CSE 8389 Theorem Proving - Seidel
Spring 2005
84
Theorem Proving
The goal is to establish
F1,…, Fk
Axioms, Assumptions
|=
T
Theorem
Show that theorem T follows from the Assumptions & Axioms F1,…, Fk
PVS operates on sequents of the form
F1,…, Fk |– G1,…, Gl
Antecedents
Consequents
Antecedents and
Consequents are
HOL Formulas
Meaning:
The disjunction of the Consequents is a logical consequence of the
conjunction of the Antecedents
F1  F2  …  Fk implies
CSE 8389 Theorem Proving - Seidel
Spring 2005
G 1  G2  …  Gl
85
Proof Trees
Sequents can be modified by PVS proof commands
F1,…, Fk |– G1,…, Gl
Antecedents
Consequents
The result of a proof command is a (possibly empty) set of subsequents
Initial sequent (show Theorem):
|-
T
The repeated application of proof commands on sequents defines a tree
A proof branch is closed if a proof command generates an empty list of
subsequents, i.e. PVS was able to validate this branch of the proof.
A theorem T is proven if all proof branches are closed.
CSE 8389 Theorem Proving - Seidel
Spring 2005
86