1
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I don't quite understand the part where you substituted value of "n" in "p" $\endgroup$ – HQuser Jun 10 at 6:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.