Transcript x - Institut für Informatik

Software Verification 1
Deductive Verification
Prof. Dr. Holger Schlingloff
Institut für Informatik der Humboldt Universität
und
Fraunhofer Institut für offene Kommunikationssysteme FOKUS
30.4.2015
By Request: Some Questions …
• What is a formal method in SW-Engineering?
• Syntax & semantics of propositional logic?
• What is a signature?
• Which calculi for PropL exist?
• How to prove correctness & completeness?
• How to prove NP-completeness?
• SAT-solving?
H. Schlingloff, Software-Verifikation I
Folie 2
H. Schlingloff, Software-Verifikation I
Folie 3
H. Schlingloff, Software-Verifikation I
Folie 4
H. Schlingloff, Software-Verifikation I
25.4.2009
Folie 5
Predicate Logic
• used to formalize mathematical reasoning
 dates back to Frege (1879) „Begriffsschrift“
- „Eine der arithmetischen nachgebildete Formelsprache des reinen
Denkens“
 individuals, predicates (sets of individuals), relations (sets
of pairs), ...
 quantification of statements (quantum = how much)
- all, none, at least one, at most one, some, most, many, ...
- need for variables to denote “arbitrary” objects
 In contrast to propositional logic, first-order logic adds
- structure to basic propositions
- quantification on (infinite) domains
H. Schlingloff, Software-Verifikation I
Folie 6
FOL: Syntax
• New syntactic elements
 R is a set of relation symbols,
where each pR has an arity nN0
 V is a denumerable set of
(first-order or individual) variables
 An atomic formula is p(x1,…,xn),
where pR is n-ary and (x1,…,xn)Vn.
• Syntax of first-order logic
FOL ::= R (Vn) |  | (FOL  FOL) | V FOL
H. Schlingloff, Software-Verifikation I
Folie 7
FOL: Syntax
• Abbreviations and parenthesis as in PL
 Of course, x = ¬x ¬
• Propositions = 0-ary relations
Predicates = 1-ary relations
 if all predicates are propositions, then FOL = PL
• Examples




xxx (p()  x(q()  p()))
xxy ¬p(x)
xy (p(x,y)  p(y,x))
(xy p(x,y)  yx p(x,y))
H. Schlingloff, Software-Verifikation I
Folie 8
Typed FOL
• Often, types/sorts are used to differentiate domains
• Signature =(D, F, R), where
•
 D is a (finite) set of domain names
 F is a set of function symbols, where each fF has an
arity nN0 and a type DDn+1
- 0-ary functions are called constants
 R is a set of relation symbols, where each pR has an
arity nN0 and a type DDn
- unary relations are called predicates
- propositions can be seen as 0-ary relations
Remark: domains and types are for ease of use only (can be
simulated in an untyped setting by additional predicates)
H. Schlingloff, Software-Verifikation I
Folie 9
Terms and Formulas
• Let again V be a (denumerable) set of (first-order) variables,
where each variable has a type DD (written as x:D)
(for any type, there is an unlimited supply of variables of that type)
• The notions Term and Atomic Formula AtF are defined
recursively:
 each variable of type D is a term of type D
 if f is an n-ary function symbol of type (D1,…Dn,Dn+1) and t1, …, tn are
terms of type D1, …, Dn, then f(t1,…,tn) is a term of type Dn+1
 if p is an n-ary relation symbol of type (D1,…Dn) and t1, …, tn are
terms of type D1, …, Dn, then p(t1,…,tn) is an atomic formula
• Revised syntax of first-order logic
FOL ::= AtF |  | (FOL  FOL) | V:D FOL
H. Schlingloff, Software-Verifikation I
Folie 10
Examples
•
•
•
•
•
x:Boy y:Girl loves(x,y)
x:Human y:Human (needs(x,y)  loves(y,x))
x,y:Int equals(plus(x,y), plus(y,x))
x:Int ¬equals(zero(), succ(x))
…
H. Schlingloff, Software-Verifikation I
Folie 11
FOL: Models
• (We give the typed semantics only)
• First-Order Model
 Let a universe U be some nonempty set, and let
DU  U for every DD be the domain of D
 Interpretation I: assignment F ↦ Un+1
R ↦ Un
 Valuation V: assignment V ↦ U
interpretations and valuations must respect typing
 Model M: (U,I,V)
H. Schlingloff, Software-Verifikation I
Folie 12
FOL: Semantics
• Given a model M: (U,I,V), the value tM of term t (of
type D) can be defined inductively
 if t=xV, then tM=V(x)
 if t=f(t1,…,tn) , then tM=I(f)(t1M,…,tnM)
• Likewise, the validation relation ⊨ between model M
and formula 
 M ⊨ p(t1,…,tn) if (t1M,…,tnM)I(p)
 M ⊭ ; M ⊨ () if M ⊨  implies M ⊨ 
 M ⊨x if M‘ ⊨ for some M‘ which differs at most in
V(x) from M
• Validity and satisfiability is defined as in the
propositional case
H. Schlingloff, Software-Verifikation I
Folie 13
Examples
•
•
•
•
•
•
⊨ x  x 
⊨ x   x   x (  )
⊨ x   x   x (  )
⊨ x y   y x 
⊨ x   (x:=t)
If ⊨ , then ⊨ x 
H. Schlingloff, Software-Verifikation I
Folie 14
FOL: Calculus
• A sound and complete axiom system for FOL:




all substitution instances of axioms of PL
modus ponens: , () ⊢ 
⊢((x:=t)x)
instantiation
() ⊢(x) if x doesn‘t occur in  particularization
• Relaxation: particularization may be applied if there is no free
occurrence of x in ; i.e., x may occur in  inside the scope
of a quantification
H. Schlingloff, Software-Verifikation I
Folie 15
FOL: Completeness
• As in the propositional case, correctness is easy
•
•
•
•
(⊢  ⊨, “every derivable formula is valid”)
Completeness (⊨  ⊢, “every valid formula is derivable”)
follows with a similar proof as previously:
given a consistent formula, construct a model satisfying it
~⊢¬  ~⊨¬
Extension lemma: If Φ is a finite consistent set of formulæ
and  is any formula, then Φ{} or Φ{¬} is consistent
Needs additionally: If Φ is any consistent set of formulæ and
x is a formula in Φ, then Φ{(t)} is consistent for any
term t
From this, a canonical model can be constructed as before
H. Schlingloff, Software-Verifikation I
Folie 16
Example
• Consider the formula
xyz ((p(x, y) ∧ p(y, z)) → p(x, z))
∧ x ¬p(x, x) ∧ x p(x, f(x) )
This formula is satifiable only in infinite models
H. Schlingloff, Software-Verifikation I
Folie 17
FOL: Undecidability
• Completeness means the set of valid formulæ can be
•
recursively enumerated
Turing showed that the invalid formulæ are not r.e.,
i.e., there is no algorithm deciding whether a
formula is valid or not
 strictly speaking, FOL= with at least one binary relation
 certain sublanguages of FOL are still decidable
H. Schlingloff, Software-Verifikation I
Folie 18
Resolution
• First “mechanizable” proof procedure (A. Robinson,
•
•
•
•
1965)
Implemented in many provers
Succeeded in proving interesting theorems
Predictability problematic (Incompleteness!)
Refutation of unsatisfiable clause sets (CNF)




Clause = finite multiset of literals
Ci={i1,..., in}  xyz(i1  ...  in)
Prove that (C1 ∧... ∧ Cm → ) by refuting {C1, ..., Cm, ¬}
Refutation means deriving the empty clause
H. Schlingloff, Software-Verifikation I
Folie 19
Propositional Resolution Rule
• From {1 ,..., m, } and {1 ,..., n, ¬}
derive {1 ,..., m, 1 ,..., n}
- In particular, from {1 ,..., m, } and {1 ,..., n, ¬}
derive {1 ,..., m}
• Corresponds to the formula
(1 ...  m  ) ∧ (1 ...  m  ¬) →
(1 ...  m  1 ...  m)
• The empty clause corresponds to ; if it is
derivable, the set of clauses is unsatisfiable
H. Schlingloff, Software-Verifikation I
25.4.2009
Folie 20
Unification
• A substitution is a mapping σ from the set of
variables to the terms such that Xσ ≠ X for only
finitely many X
- Generalizes to terms and literals
- Example: p(f(x), y){x::=a, y::=g(a)} yields p(f(a), g(a))
• σ is a unifier for terms s and t if sσ = tσ
• σ is the most general unifier if for every other unifier
•
σ‘ there exists a substitution λ such that λ σ = σ‘
Example: Unifier for p(f(x), g(z)) and p(f(a), y) is
{x::=a, y::=g(a), z::=a}
H. Schlingloff, Software-Verifikation I
25.4.2009
Folie 21
Predicate Logic Resolution
• Let C and D be clauses without overlapping
variables, {}≠PC positive literals and
{}≠ND negative literals
• Find the most general unifier σ such that
Pσ=Nσ
• Add new clause (C-P)σ(D-N)σ
• Again, if the empty clause is derivable, the set
of clauses is refuted.
H. Schlingloff, Software-Verifikation I
25.4.2009
Folie 22
FOL=
• Equality is not definable in FOL
• First order logic with equality contains an additional
(binary) relation == which is always interpreted as
equality of domain elements
 Written in infix notation, i.e. (x==y) for ==(x,y)
• Axioms




(x==x)
(x==y  (y==z  x==z))
(x==y  y==x)
(x==y  (  (y:=x)))
H. Schlingloff, Software-Verifikation I
reflexivity
transitivity
symmetry
substitution
Folie 23