A Theory of Linear Lists Push the complexity into literals ·Define new literals: linear(n=def Vq.q≠0→Vp1.p2.sel(n,p1)=sel(n,P2)=q→p1=p2 rc0(n,b)=defb≠0→p.sel(n,p)≠b Now the predicates become: Pre is linear(n)ArcO(n,b)Aa≠0Ab≠O Post is linear(n) VC is linear(n)Arc0(n,b)Aa≠0Ab≠0→ linear(upd(upd(n,a,b),b,sel(n,a))))This is a G! The hard work is now in the satisfiability procedure Prof.Necula CS 294-8 Lecture 11 11
Prof. Necula CS 294-8 Lecture 11 11 A Theory of Linear Lists • Push the complexity into literals • Define new literals: linear(n) =def q.q 0 p1 .p2 . sel(n, p1 ) = sel(n, p2 ) = q p1 = p2 rc0(n, b) =def b 0 p. sel(n, p) b • Now the predicates become: Pre is linear(n) rc0(n, b) a 0 b 0 Post is linear(n) VC is linear(n) rc0(n, b) a 0 b 0 linear(upd(upd(n, a, b), b, sel(n, a)))) This is a G ! • The hard work is now in the satisfiability procedure
A Theory of Linear Lists 。」 In order to allow the prover to work with "linear"and "rcO"we must define their meaning: Semantically(by giving the definitions from before) -Axiomatically(by giving a set of axioms that define them): linear(n) ā≠0 rcO(n,b) linear(n) a≠0 rcO(n,b) linear(upd(n,a,b)) rco(upd(n,a,b),sel(n,a)) Now we can prove the VC with just three uses of these axioms Is this set of axioms complete? Prof.Necula CS 294-8 Lecture 11 12
Prof. Necula CS 294-8 Lecture 11 12 A Theory of Linear Lists • In order to allow the prover to work with “linear” and “rc0” we must define their meaning: – Semantically (by giving the definitions from before) – Axiomatically (by giving a set of axioms that define them): linear(n) a 0 rc0(n, b) linear(upd(n, a, b)) linear(n) a 0 rc0(n, b) rc0(upd(n, a, b), sel(n, a)) • Now we can prove the VC with just three uses of these axioms • Is this set of axioms complete?