Finish Verification Condition Generation Simple Prover for FOL CS294-8 Lecture 10 Prof.Necula CS 294-8 Lecture 10 1
Prof. Necula CS 294-8 Lecture 10 1 Finish Verification Condition Generation Simple Prover for FOL CS 294-8 Lecture 10
Not Quite Weakest Preconditions Recall what we are trying to do: false → frue Pre(s,B) strong ↑1 weak weakest A precondition:WP(s,B) verification condition:VC(s,B) We shall construct a verification condition:VC(s,B) The loops are annotated with loop invariants VC is guaranteed stronger than WP But hopefully still weaker than A:A>VC(s,B)WP(s,B) Prof.Necula CS 294-8 Lecture 10 2
Prof. Necula CS 294-8 Lecture 10 2 Not Quite Weakest Preconditions • Recall what we are trying to do: false true strong weak Pre(s, B) weakest A precondition: WP(s, B) verification condition: VC(s, B) • We shall construct a verification condition: VC(s, B) – The loops are annotated with loop invariants ! – VC is guaranteed stronger than WP – But hopefully still weaker than A: A VC(s, B) WP(s, B)
Verification Condition Generation Computed in a manner similar to WP 。 Except the rule for while: VC(whiler E do s,B)= IA(X1Xn.I→(E→VC(s,I)AE→B)) I holds I is preserved in B holds when the on entry an arbitrary iteration loop terminates I is the loop invariant (provided externally) X1,...Xn are all the variables modified in s The V is similar to the V in mathematical induction: P(O)An∈N.P(n)→P(n+1) Prof.Necula CS 294-8 Lecture 10 3
Prof. Necula CS 294-8 Lecture 10 3 Verification Condition Generation • Computed in a manner similar to WP • Except the rule for while: VC(whileI E do s, B) = I (x1…xn . I (E VC(s, I) E B) ) • I is the loop invariant (provided externally) • x1 , …, xn are all the variables modified in s • The is similar to the in mathematical induction: P(0) n N. P(n) P(n+1) I holds on entry I is preserved in an arbitrary iteration B holds when the loop terminates
Forward Verification Condition Generation Traditionally VC is computed backwards Works well for structured code o But it can be computed in a forward direction Works even for low-level languages (e.g.,assembly language) Uses symbolic evaluation(important technique #2) Has broad applications in program analysis e.g.the PREfix tools works this way Prof.Necula CS 294-8 Lecture 10 4
Prof. Necula CS 294-8 Lecture 10 4 Forward Verification Condition Generation • Traditionally VC is computed backwards – Works well for structured code • But it can be computed in a forward direction – Works even for low-level languages (e.g., assembly language) – Uses symbolic evaluation (important technique #2) – Has broad applications in program analysis • e.g. the PREfix tools works this way
Symbolic Evaluation Consider the language: x:=E I f()I if E goto L goto LL:return I inv E The "inv E"instruction is an annotation Says that boolean expression E holds at that point Notation:Ik is the instruction at address k Prof.Necula CS 294-8 Lecture 10 5
Prof. Necula CS 294-8 Lecture 10 5 Symbolic Evaluation • Consider the language: x := E | f() | if E goto L | goto L | L: | return | inv E • The “inv E” instruction is an annotation – Says that boolean expression E holds at that point • Notation: Ik is the instruction at address k