Hoare-Axiome (Skip & Zuweisung)

Grundlegende Gesetze des Hoare-Kalküls:

1. Skip-Axiom: $\{P\}skip\{P\}$. Skip ändert den Zustand nicht.
2. Zuweisungsaxiom: $\{P[x\leftarrow E]\}x:=E\{P\}$.
   Man ersetzt in der Nachbedingung $P$ jedes Vorkommen der Variable $x$ durch den Ausdruck $E$, um die Vorbedingung zu erhalten (Rückwärtsschluss).
   Beispiel: $\{y+5=10\}x:=y+5\{x=10\}$.