Hoare-Inferenzregeln (Sequenz, If, Konsequenz)

Regeln zum Zusammensetzen von Programmteilen:

1. Sequenzregel:$$\frac{\{P\}{S}_1\{R\},\{R\}{S}_2\{Q\}}{\{P\}{S}_1;S_2\{Q\}}$$Die Nachbedingung des ersten Teils ist Vorbedingung des zweiten.
2. Rule of Consequence (Konsequenzregel):$$\frac{P\to P^{\prime },\{P^{\prime }\}S\{Q^{\prime }\},Q^{\prime }\to Q}{\{P\}S\{Q\}}$$Erlaubt Verschärfung der Vorbedingung ($P\to P^{\prime }$) und Abschwächung der Nachbedingung ($Q^{\prime }\to Q$).
3. If-Regel:$$\frac{\{P\wedge B\}{S}_1\{Q\},\{P\wedge \mathrm{\neg }B\}{S}_2\{Q\}}{\{P\}ifBthen{S}_{1}else{S}_{2}fi\{Q\}}$$Beweist beide Zweige unter der Annahme der Bedingung bzw. deren Negation.