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 5Prof. 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 !