How to use Hoare Logic to Prove this Assertion

Question

Given this assertion in Hoare Logic:

\begin{align} &\mathbf{\{p >= 0\}}\\ &s = 0 ; n = 1 ;\\ &\mathtt{while}\ (n <= p)\ \{\\ &\quad s = s + n ;\\ &\quad n = n + 1\\ &\}\\ &\mathbf{\{s == p * (p + 1) / 2\}} \end{align}

How to prove this using the rules of Hoare Logic. I am not sure where to really begin, I only currently understand (most) of the meaning of the axioms, but not what is required for a proof.

Answer 1

Its a question of chaining/glueing the axioms between them.

Let's start from the end:

$$\mathbf{\{s == p * (p + 1) / 2\}}$$

Use the strengthening rule to change the postcondition to

$$\mathbf{\{s == p * (p + 1) / 2 \wedge p == n \wedge p >= 0\}} $$

which is equivalent to

$$\mathbf{\{s == n * (n + 1) / 2 \wedge p == n \wedge p >= 0\}}$$

By the Loop rule in order for the triple:

$$ \mathbf{\{s == n * (n + 1) / 2 \}} \mathtt{while}\ (n <= p)\ \{s = s + n ; n = n + 1\} \mathbf{\{s == n * (n + 1) / 2 \wedge p == n \}} $$

we need to prove that the triple

$$\mathbf{\{s == n * (n + 1) / 2 \}} \{s = s + n ; n = n + 1\} \mathbf{\{s == n * (n + 1) / 2\}}$$

is valid.

Let then use the composition to reduce this to proving that the two following triples are valid:

$$\mathbf{\{s == n * (n + 1) / 2 \}} \{s = s + n\} \mathbf{\{s == (n+1) * (n + 2) / 2\}}$$

and

$$\mathbf{\{s == (n+1) * (n + 2) / 2 \}} \{ n = n + 1\} \mathbf{\{s == n * (n + 1) / 2\}}$$

The latter one is just an application of the Assignment rule (just replace the occurrences of $n$ by $n+1$ in the postcond to get the precondition).

To prove the first one, we need to apply Strengthening to reduce it to the triple $$\mathbf{\{s == n * (n + 1) / 2 \}} \{s = s + n\} \mathbf{\{s == (n) * (n +1) / 2 + n\}}$$ and then use the Assignment rule trivially.

Okay so now we only need (by Sequence rule) to prove that the triple

$$\mathbf{\{p>=0 \}} s:=0; n:= 1 \mathbf{\{s == n * (n + 1) / 2 \wedge p >= 0\}}$$ which can be done in the same way by splitting with sequence.