die die gewünschte Beziehung zwischen Ein- und Ausgabe beschreibt.
Forderung an die Ausgaben: Nachbedingung
Schreibweise: { V } A { N }
{ V } A { N }