Die Zuweisung x := x + 1 hat zwei Bedingungen: die eine Bedingung ist vor der Ausführung des Sprachkonstrukts wahr, die andere Bedingung ist nach der Ausführung wahr. Die Bedingung, die davor wahr ist, nennt man Vorbedingung (englisch: precondition) und sie wird mit P abgekürzt. Die Bedingung, die nach der Ausführung wahr ist, nennt man Nachbedingung (englisch: postcondition) und sie wird mit Q abgekürzt. Die Bedingungen werden immer in geschwungene Klammern gesetzt {}. Angewendet auf das Beispiel bedeutet das:
{x = A} x := x + 1 {x = A + 1}
oder in einer etwas anderen Schreibweise
{x = A}
x := x + 1
{x = A + 1}
Für x := 1 / y ist die Vorbedingung y != 0. Also erhält man:
{y != 0} x := 1 / y {x = 1 / y}
oder in der anderen Schreibweise
{y != 0}
x := 1 / y
{x = 1 / y}
Der Unterschied zwischen diesem Beispiel und dem Beispiel x := x + 1 ist der, dass in diesem Beispiel y != 0 die Vorraussetzung für die Ausführung von x := 1 / y ist, in dem anderen Beispiel ist x = A keine "echte" Bedingung, diese Vorbedingung stellt nur den Bezug zu dem Wert von x vor der Ausführung dar.
Es müssen aber nicht immer nur Zuweisungen als Programmkonstrukt C angegeben werden, in diesem Beispiel wird das Vertauschen von x und y durch den Pseudocode "swapxy" vorgenommen:
{x = X and y = Y}
swapxy
{x = Y and y = X}
Dies bedeutet, dass vor der Ausführung von swapxy x den Wert X und y den Wert Y hatte. Nach dem Aufruf swapxy hat x den Wert Y und y den Wert X.
Die axiomatische Semantik kann gut benutzt werden, um Verhalten von Programmen zu spezifizieren, wie schon in dem letzten Beispiel gezeigt wurde. Um das Sortieren eines Feldes zu spezifizieren reicht z.B. folgendes:
{n >= 1 and for all i, 1 <= i <= n, a[i] = A[i]}
sort-program
{sorted(a) and permutation(a, A)}
Dies sagt aus, dass wir als Vorbedingung zwei Felder hatten, die die gleichen Elemente an den gleichen Stellen des Feldes hatten. Nach dem Aufruf von "sort-program" ist das Feld a nach dem Sortieralgorithmus umsortiert worden (dies wird überprüft mit sorted(a)) und das Feld a enthält noch alle Elemente, die auch in dem Feld A enthalten sind (dies wird durch permutation(a, A) deutlich gemacht). Das Feld a ist also umsortiert worden.