Hoare-Kalkül
Hoare-Kalkül

== Hoare-Tripel ==
Das zentrale Element des Hoare-Kalküls ist das Hoare-Tripel, das beschreibt, wie ein Programmteil den Zustand einer Berechnung verändert:
Dabei sind  und  Zusicherungen (englisch ''assertions''),  ist ein Programmsegment.  ist die Vorbedingung (englisch ''precondition'') und  die Nachbedingung (englisch ''postcondition''). Wenn die Vorbedingung zutrifft, gilt nach der Ausführung des Programmsegments die Nachbedingung. Zusicherungen sind Formeln der Prädikatenlogik.
Ein Tripel kann auf folgende Weise verstanden werden: Falls  für den Programmzustand vor der Ausführung von  gilt, dann gilt  danach. Falls  nicht terminiert, dann gibt es kein danach, also kann in diesem Fall  jede beliebige Aussage sein. Tatsächlich kann man für  die Aussage ''falsch'' wählen, um auszudrücken, dass  nicht terminiert. Man spricht hier von partieller Korrektheit. Falls  immer terminiert und danach  wahr ist, spricht man von totaler Korrektheit. Die Terminierung muss unabhängig bewiesen werden.
Falls keine Vorbedingung existiert, schreibt man: