Benutzer-Werkzeuge

Webseiten-Werkzeuge


glossar:annotationsbeweis

Unterschiede

Hier werden die Unterschiede zwischen zwei Versionen gezeigt.

Link zu dieser Vergleichsansicht

glossar:annotationsbeweis [2017/09/26 10:20] (aktuell)
Zeile 1: Zeile 1:
 +====== Annotationsbeweis ======
 +//engl.:// **proof outline**
 +===== Bedeutung ======
 +Annotiere das Programm so mit Zusicherungen,​ dass:
 +  * vor und hinter jeder Anweisung mindestens eine Zusicherung steht und
 +  * die Hoare-Regeln erfüllt sind.
 +
  
glossar/annotationsbeweis.txt · Zuletzt geändert: 2017/09/26 10:20 (Externe Bearbeitung)