Symbolic Evaluation.Putting it all together ·Let X1,..Xn be all the variables and a1,..an fresh parameters -2 be the state[X1=a1,…,×n=an] -Φbe the empty Inv set For all functions f in your program,compute a1an.o(Prer)→VC(f,o,φ) If all of these predicates are valid then: - If you start the program by invoking any f in a state that satisfies Pref the program will execute such that At all "inv E"the E holds,and If the function returns then Post;holds Can be proved w.r.t.a real interpreter (operational semantics) Prof.Necula CS 294-8 Lecture 10 11
Prof. Necula CS 294-8 Lecture 10 11 Symbolic Evaluation. Putting it all together • Let – x1 , …, xn be all the variables and a1 , …, an fresh parameters – S0 be the state [x1 := a1 , …,xn :=an ] – be the empty Inv set • For all functions f in your program, compute a1…an . S0 (Pref ) VC(fentry, S0 , ) • If all of these predicates are valid then: – If you start the program by invoking any f in a state that satisfies Pref the program will execute such that • At all “inv E” the E holds, and • If the function returns then Postf holds – Can be proved w.r.t. a real interpreter (operational semantics)
VC Generation Example Consider the program 1:I:=0 Precondition:B:bool AA array(bool,L) R:=B 3:invI≥0∧R:bool ifI≥goto9 assert saferd(A+I) T:=*(A+) I:=I+1 R:=T 90to3 9:return R Postconditon:R:bool Prof.Necula CS 294-8 Lecture 10 12
Prof. Necula CS 294-8 Lecture 10 12 VC Generation Example • Consider the program 1: I := 0 Precondition: B : bool A : array(bool, L) R := B 3: inv I 0 R : bool if I L goto 9 assert saferd(A + I) T := *(A + I) I := I + 1 R := T goto 3 9: return R Postconditon: R : bool
VC Generation Example (cont.) ∀A.∀B.∀l.u. B bool A array(bool,L) 0≥0AB:b0olA VI.VR. I≥0AR:bool→ I≥L→R:bool Λ I<L→saferd(A+I)A I+120Λ sel(u,A I)bool VC contains both proof obligations and assumptions about the control flow Prof.Necula CS 294-8 Lecture 10 13
Prof. Necula CS 294-8 Lecture 10 13 VC Generation Example (cont.) A. B. L. m. B : bool A : array(bool, L) 0 0 B : bool I. R. I 0 R : bool I L R : bool I < L saferd(A + I) I + 1 0 sel(m, A + I) : bool • VC contains both proof obligations and assumptions about the control flow
Review We have defined weakest preconditions Not always expressible Then we defined verification conditions Always expressible Also preconditions but not weakest =loss of completeness Next we have to prove the verification conditions But first,we'll examine some of their properties Prof.Necula CS 294-8 Lecture 10 14
Prof. Necula CS 294-8 Lecture 10 14 Review • We have defined weakest preconditions – Not always expressible • Then we defined verification conditions – Always expressible – Also preconditions but not weakest => loss of completeness • Next we have to prove the verification conditions • But first, we’ll examine some of their properties
VC and Invariants Consider the Hoare triple: {x≤O}whiler×≤5do×←-×+1{x≥6} ·The VC for this is: ×≤0→I(X)ΛX.(I(X)→(X>5→×≥6Λ ×≤5→(X+1)) Requirements on the invariant: Holds on entry X.×≤0→(x) -Preserved by the body∀x.I(x)∧x≤5→I(x+1) Useful Vx.I(X)A×>5→×≥6 ·Check that I(x)=X≤6 works And is the only one that satisfies all constraints Prof.Necula CS 294-8 Lecture 10 15
Prof. Necula CS 294-8 Lecture 10 15 VC and Invariants • Consider the Hoare triple: {x 0} whileI x 5 do x x + 1 {x 6} • The VC for this is: x 0 I(x) x. (I(x) (x > 5 x 6 x 5 I(x+1) )) • Requirements on the invariant: – Holds on entry x. x 0 I(x) – Preserved by the body x. I(x) x 5 I(x+1) – Useful x. I(x) x > 5 x 6 • Check that I(x) = x 6 works – And is the only one that satisfies all constraints