Problem 13 - Hoare's Axioms

Consider the Hoare's axioms to prove the correctness of a program.

1.

Give the axiom of the assignment statement.

2.

Give the inference rule of the while statement.

3.

Give the inference rule for the if-then-else statement.

4.

Using the fact that the while statement can be constructed from the goto statement and the if-then-else statement, show that the rule of (2) can be derived from the rule of (3) and the following rule for the goto statement:

$S \{ \hbox{goto} \; l \} \hbox{false} \vdash P \{ Q_1 \} S$

$S \{ \hbox{goto} \; l \} \hbox{false} \vdash S \{ Q_2 \} R$

$P \{ Q_1; l: Q_2 \} R$

1.

$$\{ p(x) \{ x \leftarrow t\} \} \texttt{x := t} \{ p(x)\}$$

2.

$$\frac{\{p\wedge B\}\texttt{S}\{p\}}{\{p\}\texttt{while B do S}\{p\wedge \neg B\}}$$

3.

$$\frac{\{p\wedge B \}\texttt{S1}\{q\} \quad \{p\wedge \neg B\}\texttt{S2}\{q\}}{\{p\}\texttt{if B then S1 else S2}\{q\}}$$

4.