In <sw-function-desc> kann eine detaillierte Beschreibung der Funktion erfolgen. Diese wird i.d.R. manuell erstellt. Formale, automatisch erstellte Anteile sollten in <sw-function-def> abgelegt werden. Unter <prms> können auch formale Parameter eingegeben werden, welche dann auch maschinell prüfbar sind. Dies betrifft Randbedingungen, Eigenschaften einer Funktion, welche nicht in <sw-param> spezifiziert werden, weil sie fest im Programm codiert sind, oder sich gar aus der Implementierungstechnik ergeben.