How to use Hoare Logic to Prove this Assertion Given this assertion in Hoare Logic:

\begin{align}
&amp;\mathbf{\{p &gt;= 0\}}\\
&amp;s = 0 ; n = 1 ;\\
&amp;\mathtt{while}\ (n &lt;= p)\ \{\\
&amp;\quad s = s + n ;\\
&amp;\quad n = n + 1\\
&amp;\}\\
&amp;\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.
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 &gt;= 0\}} $$

which is equivalent to 

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

By the Loop rule in order for the triple:

$$ \mathbf{\{s == n * (n + 1) / 2 \}} \mathtt{while}\ (n &lt;= 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&gt;=0 \}} s:=0; n:= 1 \mathbf{\{s == n * (n + 1) / 2 \wedge p &gt;= 0\}}$$
which can be done in the same way by splitting with sequence.