Theorem Proving for FOL Satisfiability Procedures CS294-8 Lecture 11 Prof.Necula CS 294-8 Lecture 11 1
Prof. Necula CS 294-8 Lecture 11 1 Theorem Proving for FOL Satisfiability Procedures CS 294-8 Lecture 11
Review Recall the we use the following logic: Goals: G::=LI true GiAG2 H>G VX.G Hypotheses: H :=L true HiA H2 Literals: L:=p(E1,....Ek) Expressions: E ::nI f(E1,...Em) This is sufficient for VCGen iff: The invariants,preconditions and postcond.are all from H Prof.Necula CS 294-8 Lecture 11 2
Prof. Necula CS 294-8 Lecture 11 2 Review • Recall the we use the following logic: Goals: G ::= L | true | G1 G2 | H G | x. G Hypotheses: H ::= L | true | H1 H2 Literals: L ::= p(E1 , …, Ek ) Expressions: E ::= n | f(E1 , …, Em) • This is sufficient for VCGen iff: – The invariants, preconditions and postcond. are all from H
A Simple and Complete Prover Define the following symbolic "prove"algorithm Prove(H,G)-prove the goal "H=G" Prove(H,true) true Prove(H,G1AG2)=prove(H,G1)&&prove(H,G2) Prove(H,Hi=G2)=prove(HA H1,G2) Prove(H,Vx.G) prove(H,G[a/x])(a is "fresh") Prove(H,L) unsat(HA-L) We have a simple,sound and complete prover If we have a way to check unsatisfiability of sets of literals Prof.Necula CS 294-8 Lecture 11 3
Prof. Necula CS 294-8 Lecture 11 3 A Simple and Complete Prover • Define the following symbolic “prove” algorithm – Prove(H, G) - prove the goal “H G” Prove(H, true) = true Prove(H, G1 G2 ) = prove(H, G1 ) && prove(H, G2 ) Prove(H, H1 G2 ) = prove(H H1 , G2 ) Prove(H, x. G) = prove(H, G[a/x]) (a is “fresh”) Prove(H, L) = unsat(H L) • We have a simple, sound and complete prover – If we have a way to check unsatisfiability of sets of literals
How Powerful is Our Prover? With VCGen in mind we must restrict invariants to H::=L true HiAH2 No disjunction,implication or quantification Is that bad Consider the function: void insert(LIST*a,LIST*b){ LIST*t=a->next;a->next=b;b->next=t; And the problem is to verify that It preserves linearity:all list cells are pointed to by at most one other list cell Provided that b is non-NULL and not pointed to by any cell Prof.Necula CS 294-8 Lecture 11 4
Prof. Necula CS 294-8 Lecture 11 4 How Powerful is Our Prover? • With VCGen in mind we must restrict invariants to H ::= L | true | H1 H2 • No disjunction, implication or quantification ! – Is that bad ? • Consider the function: void insert(LIST *a, LIST * b) { LIST *t = a->next; a->next = b; b->next = t; } • And the problem is to verify that – It preserves linearity: all list cells are pointed to by at most one other list cell – Provided that b is non-NULL and not pointed to by any cell
Lists and Linearity A bit of formal notation (remember the sel/upd): We write sel(n,a)to denote the value of "a->next"given the state of the "next"field is "n" We write upd(n,a,b)to denote the new state of the "next" field after "a->next b" Code is void insert(LIST*a,LIST*b){ LIST*t=a->next;a->next b;b->next =t; Pre is(付q.q≠0→p1.∀p2.sel(n,p1)=sel(n,p2)=q→p1=p2) Ab≠0∧p.sel(n,p)≠bAa≠0 Post is(q.q≠0→Vp1.∀p2.sel(n,p1)=sel(n,P2)=q→p1=p2) VC is Pre=Post[upd(upd(n,a,b),b,sel(n,a))/n]Not aG! Prof.Necula CS 294-8 Lecture 11 5
Prof. Necula CS 294-8 Lecture 11 5 Lists and Linearity • A bit of formal notation (remember the sel/upd): – We write sel(n, a) to denote the value of “a->next” given the state of the “next” field is “n” – We write upd(n, a, b) to denote the new state of the “next” field after “a->next = b” Code is void insert(LIST *a, LIST * b) { LIST *t = a->next; a->next = b; b->next = t; } Pre is (q.q 0 p1 .p2 .sel(n, p1 ) = sel(n, p2 ) = q p1 = p2 ) b 0 p.sel(n, p) b a 0 Post is (q. q 0 p1 .p2 . sel(n, p1 ) = sel(n, p2 ) = q p1 = p2 ) VC is Pre Post[upd(upd(n, a, b), b, sel(n, a)) / n] Not a G !