glossar:prozedurspezifikation
Prozedurspezifikation
Bedeutung
Eine Prozedurspezifikation besteht aus:
einer Vorbedingung: requires <Ausdruck>
einer Variablenliste: modifies <Liste von Variablen>
einer Nachbedingung: ensures <Ausdruck>
Bemerkungen
Für eine leere Variablenliste schreibt man „\nothing“.
Eine Prozedur darf nur die globalen Variablen und Verbundkomponenten/Instanzvariablen verändern, die in der Variablenliste aufgeführt sind.
glossar/prozedurspezifikation.txt · Zuletzt geändert: 2016/09/22 10:14 (Externe Bearbeitung)