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.