repeat bn1 := removeBean() bn2 := removeBean() if (bn1.col == white) ∧ (bn2.col == white) then putBlack() elsif (bn1.col == black) ∧ (bn2.col == black) then putBlack() else putWhite()

input/output ? preconditions ? postconditions ?

**variant**nonneg. int. expression, decreases each iteration

**invariant**expresssion, holds each time execution reaches it

**a ≡ b (mod n)**

a, b ∈ n ∈ ∃ z ∈ , a = b + n ⋅ z (so a,b differ by a multiple of n)

exercise

let w_{k},b_{k}:
number white,black beans after k iterations

let W,B: number white,black beans at start
(so W=w_{0}, B=b_{0})

use definition of *mod*

assume w_{k} =
W (mod 2) and w_{k+1} = w_{k} - 2

prove w_{k+1} = W (mod 2)

# w/b: white/black beans in tin # precondition: pos. int. W,B w := W b := B while # invariant: w + b ≥ 1 # invariant: w ≡ W (mod 2) # variant: w + b w + b > 1 do bn1 := removeBean() bn2 := removeBean() if (bn1.col == white) ∧ (bn2.col == white) then putBlack() elsif (bn1.col == black) ∧ (bn2.col == black) then putBlack() else putWhite() endif endwhile # postcondition: w + b = 1 # postcondition: w ≡ W (mod 2)

proof of 1st invariant (by induction) (sketch)

w_{t}, b_{t} ≡ value of w,b
after t iterations of loop body

**1st time**execution reaches inv. pointw

_{0}= W ≥ 1 b_{0}= B ≥ 1 so

w_{0}+ b_{0}= W + B ≥ 1 + 1 ≥ 1**(k+1)st time**execution reaches inv. pointexecution passed while guard/test, so

w_{k}+ b_{k}> 1 so w_{k}+ b_{k}≥ 2**case 1**(bn1.col == white) ∧ (bn2.col == white)w

_{k+1}+ b_{k+1}= (w_{k}- 2) + (b_{k}+1) = w_{k}+ b_{k}- 1 ≥ 1**case 2**(bn1.col == black) ∧ (bn2.col == black)exercise

**case 3**(else)w

_{k+1}+ b_{k+1}= w_{k}+ b_{k}- 1 = w_{k}+ b_{k}- 1 ≥ 1

so, by induction, invariant holds each time execution reaches it

proof of 2nd invariant (by induction) (sketch)

**1st time**

w_{0} = W so w_{0} ≡ W (mod 2)

**(k+1)st time**

assume inv. holds k'th time, so w_{k} ≡ W (mod 2)

**case 1**

w_{k+1} = w_{k} - 2 ≡ W - 2 (mod 2) ≡ W (mod 2)

**case 2**

(exercise)

**case 3**

w_{k+1} = w_{k} ≡ W (mod 2)

so, by induction, invariant holds each time execution reaches it

variant valid (proof by induction) (sketch)

**want to show**

variant stays nonneg. and always decreases

**1st time**

by above, w_{0}+b_{0} ≥ 1 so non-neg.

**(k+1)st time**

by above, in each case w_{k+1} + b_{k+1} = w_{k} + b_{k} - 1 so variant decreases

execution crossed guard so w_{k} + b_{k} ≥ 2 so w_{k+1} + b_{k+1} ≥ 1

**loop terminates**

variant x+y

**w + b = 1**

w + b ≥ 1 (last variant) and w + b ≯ 1 (failed guard)

**last bean color**

white ⇔ W ≅ 1 (mod 2)

while w + b > 1 do bn1 := removeBean() bn2 := removeBean() if (bn1.col == black) ∧ (bn2.col == black) then putBlack() elsif (bn1.col != bn2.col) then putWhite()

exercise

assume: b,w start non-negative, body executes t times

describe final b

_{t},w_{t}in terms of starting b_{0},w_{0}hint: possibilities for b

_{t},w_{t}are 0,0 0,1 1,0

w_{0} is odd ?

b

_{t},w_{t}= 0,1

w_{0} is even ?

b

_{0}= 0 ⇒ b_{t},w_{t}= 0,0b

_{0}≥ 1 ∧ w_{0}= 0 ⇒ b_{t},w_{t}= 1,0b

_{0}≥ 1 ∧ w_{0}≥ 2 ⇒ b_{t},w_{t}= 0,0 or 1,0 in every case, both are possible (prove this)