# beans (variants and invariants)

beans, loops, example, inv.1, inv.2, var., post., another,

### coffee beans

```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 wk,bk: number white,black beans after k iterations

let W,B: number white,black beans at start   (so W=w0, B=b0)

use definition of mod

assume wk = W (mod 2)     and     wk+1 = wk - 2

prove wk+1 = W (mod 2)

### simple example

```# 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)
```

### 1st invariant

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

wt, bt ≡   value of w,b after t iterations of loop body

1st time execution reaches inv. point

w0 = W ≥ 1   b0 = B ≥ 1     so
w0 + b0 = W + B ≥ 1 + 1 ≥ 1

(k+1)st time execution reaches inv. point

execution passed while guard/test, so
wk + bk > 1   so  wk + bk ≥ 2

case 1 (bn1.col == white) ∧ (bn2.col == white)

wk+1 + bk+1   =   (wk - 2) + (bk+1)   =   wk + bk - 1   ≥ 1

case 2 (bn1.col == black) ∧ (bn2.col == black)

exercise

case 3 (else)

wk+1 + bk+1   =   wk + bk - 1   =   wk + bk - 1   ≥   1

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

### 2nd invariant

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

1st time
w0 = W   so   w0 ≡ W (mod 2)

(k+1)st time
assume inv. holds k'th time, so wk ≡ W (mod 2)

case 1
wk+1   =   wk - 2   ≡   W - 2 (mod 2)   ≡   W (mod 2)

case 2
(exercise)

case 3
wk+1   =   wk   ≡   W (mod 2)

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

### variant

variant valid (proof by induction) (sketch)

want to show
variant stays nonneg. and always decreases

1st time
by above, w0+b0 ≥ 1   so non-neg.

(k+1)st time
by above, in each case wk+1 + bk+1 = wk + bk - 1   so variant decreases
execution crossed guard   so wk + bk ≥ 2   so wk+1 + bk+1 ≥ 1

### postconditions

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)

### another example

```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 bt,wt in terms of starting b0,w0

• hint: possibilities for bt,wt are   0,0   0,1   1,0

w0 is odd ?

• bt,wt = 0,1

w0 is even ?

• b0 = 0   ⇒   bt,wt = 0,0

• b0 ≥ 1   ∧ w0 = 0   ⇒   bt,wt = 1,0

• b0 ≥ 1   ∧ w0 ≥ 2   ⇒   bt,wt = 0,0   or   1,0       in every case, both are possible (prove this)