Hier werden die Unterschiede zwischen zwei Versionen gezeigt.
— |
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. | ||
+ | |||