Lecture #42: More on Program VerificationLoopsExampleGetting to the LoopInvent a Loop InvariantEstablish the invariantDoes the Invariant give us the desired result?Invariance of the InvariantAn ApplicationLecture #42: More on Program Verification• Rules so far:{P } pass {P }P ⇒ R, {R} S {Q}{P } S {Q}R ⇒ Q, {P } S {R}{P } S {Q}{P ∧ C} S1 {Q}, {P ∧ not C} S2 {Q}{P } if C: S1; else: S2 {Q}P ⇒ Q[x ← E]{P } x = E {Q}{P } S1 {R}, {R} S2 {Q}{P } S1;S2 {Q}• We’re assuming that expressions (as opposed to s ta tements) haveno side-effects.• And now come the hard ones. . .Last modified: Thu May 5 22:46:23 2005 CS164: Lecture #42 1Loops• Simple while loops take some invention.• Classical technique is to invent aloop invariant—an a ssertion thatdescribes how things look at the start of an arbitrary iteration.• For example,while i < len(A):{ A[0..i] is sorted } ⇐= Loop invariantcode to swap A[i] with largest element in A[0..i+1]i += 1• End up with a rule like this:P ⇒ I, {I ∧ C} S {I}, I ∧ not C ⇒ Q{P } while C: S {Q}Last modified: Thu May 5 22:46:23 2005 CS164: Lecture #42 2Example• We want demonstrate the following (“The Russian Peasant’s Algo-rithm”), ignoring integer overflow:{ n ≥ 0 ∧ x 6= 0 }i = n; p = x; y = 1while i > 0:if i % 2 == 1: y = y*pi = i/2; p = p*p{ y = xn}Last modified: Thu May 5 22:46:23 2005 CS164: Lecture #42 3Getting to the Loop• First, let’s get an assertion at the beginning of the while loop tomake it more convenient to use the rule:{ n ≥ 0 ∧ x 6= 0 }i = n; p = x; y = 1{ i = n ≥ 0 ∧ p = x 6= 0 ∧ y = 1 }while i > 0:if i % 2 == 1: y = y*pi = i/2; p = p * p{ y = xn}• Using the assignment rule three times, must show thatn ≥ 0 ∧ x 6= 0 ⇒ n = n ≥ 0 ∧ x = x 6= 0 ∧ 1 = 1. . . which is pretty obvious.Last modified: Thu May 5 22:46:23 2005 CS164: Lecture #42 4Invent a Loop Invariant• The i dea behind this loop was to use the fact that a2b= a · (a2)b.• At th e beginning of each iter ation, we are left w i th computing pi.• Suggesting th i s invariant:{ n ≥ 0 ∧ x 6= 0 }i = n; p = x; y = 1{ i = n ≥ 0 ∧ p = x 6= 0 ∧ y = 1 }while i > 0: { i ≥ 0 ∧ p 6= 0 ∧ pi· y = xn}if i % 2 == 1: y = y*pi = i/2; p = p * p{ y = xn}Last modified: Thu May 5 22:46:23 2005 CS164: Lecture #42 5Establish the invariant{ n ≥ 0 ∧ x 6= 0 }i = n; p = x; y = 1{ i = n ≥ 0 ∧ p = x 6= 0 ∧ y = 1 }while i > 0: { i ≥ 0 ∧ p 6= 0 ∧ pi· y = xn}if i % 2 == 1: y = y*pi = i/2; p = p*p{ y = xn}According to the while rule, must first showi = n ≥ 0 ∧ p = x 6= 0 ∧ y = 1 ⇒ i ≥ 0 ∧ p 6= 0 ∧ pi· y = xn≡i = n ≥ 0 ∧ p = x 6= 0 ∧ y = 1 ⇒ n ≥ 0 ∧ x 6= 0 ∧ xn· 1 = xn. . . which is obvious.Last modified: Thu May 5 22:46:23 2005 CS164: Lecture #42 6Does the Invariant give us the desired result?{ n ≥ 0 ∧ x 6= 0 }i = n; p = x; y = 1{ i = n ≥ 0 ∧ p = x 6= 0 ∧ y = 1 }while i > 0: { i ≥ 0 ∧ p 6= 0 ∧ pi· y = xn}if i % 2 == 1: y = y*pi = i/2; p = p*p{ y = xn}Last part of while rule requires that we show that when the loopcondition is false, i nvariant implies conclusion:i ≥ 0 ∧ p 6= 0 ∧ pi· y = xn∧ i ≤ 0 ⇒ y = xn≡since only 0 is both≥ 0and≤ 0i = 0 ∧ p 6= 0 ∧ p0· y = xn⇒ y = xnAgain, pretty clear (if tedious).Last modified: Thu May 5 22:46:23 2005 CS164: Lecture #42 7Invariance of the Invariant{ n ≥ 0 ∧ x 6= 0 }i = n; p = x; y = 1{ i = n ≥ 0 ∧ p = x 6= 0 ∧ y = 1 }while i > 0: { i ≥ 0 ∧ p 6= 0 ∧ pi· y = xn}if i % 2 == 1: y = y*pi = i/2; p = p*p{ y = xn}• Finally, need to show that if i > 0, executing the loop preserves theinvariant.• Applying assignment and if rules, we end up having to demonstra tethe following (which I leave to you (:->)):i ≥ 0 ∧ p 6= 0 ∧ pi· y = xn∧ i > 0 ∧ i mod 2 = 1⇒ bi/2c ≥ 0 ∧ p26= 0 ∧ p2bi/2c· y · p = xnandi ≥ 0 ∧ p 6= 0 ∧ pi· y = xn∧ i > 0 ∧ i mod 2 6= 1⇒ bi/2c ≥ 0 ∧ p26= 0 ∧ p2bi/2c· y = xnLast modified: Thu May 5 22:46:23 2005 CS164: Lecture #42 8An Application• Very tedi ous, as you can see, and therefore error-prone.• Even worse, turns programs into reall y complicated theorems, buttheorem provers are not up to the task.• Proof checkers, on the other hand, are pretty ea sy to build (give mean alledged formal proof, a nd I’ll check it).• One application: proof-carrying code:– Un trusted party provides, e.g., device driver, with an alleged proofthat the driver adheres to your system’s requirements of whatnot to mess with.– Your (trusted) proof checker checks that their proof actuallycomes from their program and is correct.Last modified: Thu May 5 22:46:23 2005 CS164: Lecture #42
View Full Document
Unlocking...