How to use Hoare Logic to Prove this Assertion
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.