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: 24.09.2014 16:47 (Externe Bearbeitung)
 
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki