Benutzer-Werkzeuge

Webseiten-Werkzeuge


glossar:hoare-triple

Hoare-Triple

engl.: Hoare triple

Bedeutung

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).

glossar/hoare-triple.txt · Zuletzt geändert: 2017/09/26 10:20 (Externe Bearbeitung)

Seiten-Werkzeuge