Eine Prozedurspezifikation besteht aus:
einer Vorbedingung: requires <Ausdruck>
einer Variablenliste: modifies <Liste von Variablen>
einer Nachbedingung: ensures <Ausdruck>
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.
