Hoare-Triple

engl.: Hoare triple

Zeige, dass die Ausführung von A

• beginnend in Vorzuständen, in denen P gilt,
• bei Terminierung in Nachzuständen endet, in denen Q gilt.

Abkürzend schreibt man dafür üblicherweise: { P } A { Q }

Zur formalen Verifikation von Hoare-Tripeln benutzt man eine Hoare-Logik oder den WP-Kalkül (siehe GdP).