Die Zusicherungsmethode nach Hoare kann für die Spezifikation (siehe Spezifikationsmethode) oder den Nachweis der partiellen Korrektheit eines Programmfragments genutzt werden. In letzterem Fall wird der Beweis über zwei Prädikate, die Vor- und die Nachbedingung geführt.

Abhängig von der Art des Programmfragments gibt es Regeln für zusammenpassende Vor- und Nachbedingungen:

• Zuweisung x := e des Werts eines Ausdrucks e an eine Variable x: {P[x / e]} x := e {P}
• Sequenz S; T zweier Programmfragmente S und T: {P} S {Q} & {Q} T {R} → {P} S; T {R}
• Bedingte Anweisung if c then S else T: {P & c} S {Q} & {P & ~c} T {Q} → {P} if c then S else T {Q}
• Schleife while c do S end while: {P & c} S {P} → {P} while c do S end while {P & ~c}, hier heisst P auch Schleifeninvariante

Außerdem gibt es zwei allgemeine Regeln zur Implikation:

• ({P} S {Q} & Q → R) → {P} S {R}
• ({P} S {Q} & R → P) → {R} S {Q}

Dabei steht die Notation {P} S {Q} für die Aussage, dass wenn vor der Ausführung des Programmfragments S die Bedingung P gilt, nach der Ausführung die Bedingung Q gilt. Die Bedingungen P und Q sind in der Regel Aussagen über die Variablen des Programms (den Zustand des Programms).

Mit Hilfe der Vor- und Nachbedingungen lässt sich die Semantik des Programmfragments beschreiben. Diese Art der Beschreibung heisst axiomatische Semantik (Prädikatensemantik).