Massachusetts Institute of Technology Department of Electrical Engineering and Computer Science

6.170 Handed Out: Thursday, November 16, 1989 Problem Set 4 — Handout Due: Wednesday, November 29, 1989

Program Verification

Marc Horowitz

initial assertion: x > 0

Proof of assignment:

y := x

x > 0
{ y := x }
(y > 0) & (x = y)

x > 0 ⟹ (x > 0) & (x = x) TRUE

Proof of assignment:

z := 0

\begin{aligned}& TRUE \\ \{ & z := 0 & \} \\ & z = 0 \end{aligned}

TRUE ⟹ 0 = 0 TRUE

Proof of while loop:

while y < 0 do
   y := y - 2
   z := z + 1
   end

loop invariant: 2 * z = x - y decrementing function: d_{n} = y over the range y ≥ -1

P ⟹ Inv

6.170 Problem Set 4 Wednesday, November 29, 1989

(y > 0) & (z = 0) (x = y) ⟹ 2 * z = x - y
(y > 0) & (z = 0) (x = y) ⟹ 0 = 0

TRUE

Inv {b} Inv

2 * z = x - y

{ y > 0 }

2 * z = x - y

2 * z = x - y ⟹ 2 * z = x - y TRUE

Inv & b {S} Inv

(2 * z = x - y) & (y > 0)
{  y := y - 2
z := z + 1  }

(2 * z = x - y) (2 * z = x - y) & (y > 0)

{ y := y - 2 }

(2 * (z + 1) = x - y)

(2 * z = x - y) & (y > 0) ⟹ (2 * (z + 1) = x - y + 2) ; (2 * z = x - y) & (y > 0) ⟹ (2 * z + 2 = x - y + 2)

TRUE

(Inv & ¬ b) ⟹ Q

\frac{(2 * z = x - y) & (y ≤ 0) ⟹ (2 * z = x - y)}{TRUE}

while b do S end terminates

Decrementing function is decremented by the body:

(y = d_{0}) & (y > 0)
{  y := y - 2
z := z + 1  }
y < d_{0}
(y = d_{0}) & (y > 0)
{ y := y - 2 }
y < d_{0}

(y = d_{0}) & (y > 0) ⟹ y - 2 < d_{0} TRUE

Test does not increment decrementing function:

\begin{aligned}& y = d_{0} \\ \{ & y > 0 & \} \\ & y ≤ d_{0} \end{aligned}

y = d_{0} ⟹ y ≤ d_{0} TRUE

When decrementing function reaches -1, the loop terminates:

\frac{(y = -1) ⟹ y ≤ 0}{TRUE}

Proof of conditional:

if y = 0 then isEven := true else isEven := false end

side-effect-free(b)

\frac{side-effect-free(y > 0)}{TRUE}

P & b {s1} Q

(2 * z = x - y) & (y ≤ 0) & (y ≥ -1) & (y = 0)
{ isEven := TRUE }

isEven = (2 * z = x)

(2 * z = x - y) & (y ≤ 0) & (y ≥ -1) & (y = 0) ⟹ TRUE = (2 * z = x) TRUE

P & ¬ b {s2} Q

(2 * z = x - y) & (y ≤ 0) & (y ≥ -1) & (y ≠ 0)
{ isEven := FALSE }

isEven = (2 * z = x)

(2 * z = x - y) & (y ≤ 0) & (y ≥ -1) & (y ≠ 0) ⟹ FALSE = (2 * z = x) TRUE

Final assertion: isEven = (2 * z = x)

QED