A detailed description of the function can follow in <sw-function-desc>. As a rule, this is prepared manually and the automatically generated components should be stored in <sw-function-def>. Formal parameters can also be entered in <prms> and these can be tested automatically. This concerns secondary conditions, i.e. properties for a function that are not specified in <sw-param> because they are permanently coded in the program or are not given at all from the implementation technique.