Example

Prove the following is correct:

$$\langle \; \rangle \; c := a+b; c := c/2 \; \langle c = (1+b)/2 \rangle$$

(assume $a,b,c$ are Real-valued)

Proof. Work backwards: ``feed'' the postcondition back through the code. Thus, by assignment rule,

$$\langle c = a + b \rangle (=) \langle c/2 = (a+b)/2 \rangle \; c := c/2 \; \langle c = (a+b)/2 \rangle$$

But so is:

$$\langle \; \rangle \Leftrightarrow \langle a+b = a+b \rangle \; c := a+b \; \langle c = a+b \rangle$$

by Assignment. We can now use the Concatenation Rule:

$$\frac{\langle \; \rangle \; c := a+b \; \langle c = a+b \rangle ,... ...{\langle \; \rangle \; c := a+b; c:=c/2 \; \langle c = \frac{a+b}{2} \rangle }$$

Typically we would set out such a proof ``Vertically'':

$$\langle a+b = a+b \rangle \Leftrightarrow \langle \; \rangle$$

$$c := a+b;$$

$$\langle c/2 = \frac{a+b}{2} \rangle \Leftrightarrow \langle c = a+b \rangle$$

$$c := c/2$$

$$\langle c = \frac{a+b}{2} \rangle$$

$\qedsymbol$

The method easily extends to arbitrary long concatenations.