Benutzer-Werkzeuge

Webseiten-Werkzeuge


glossar:hoare-triple

Unterschiede

Hier werden die Unterschiede zwischen zwei Versionen gezeigt.

Link zu dieser Vergleichsansicht

glossar:hoare-triple [2017/09/26 10:20] (aktuell)
Zeile 1: Zeile 1:
 +====== 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)