Benutzer-Werkzeuge
glossar:annotationsbeweis
Unterschiede
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. | ||
| + | |||
glossar/annotationsbeweis.txt · Zuletzt geändert: 2017/09/26 10:20 (Externe Bearbeitung)
Seiten-Werkzeuge
