Function specifications

VeriFast accepts the following specification clauses between a function's header and its body:

^Syntax
SpecificationClause :
      /*@ req Assertion ; @*/
   | /*@ ens Assertion ; @*/
   | /*@ on_unwind_ens Assertion ; @*/
   | /*@ assume_correct @*/

Note that VeriFast also support single-line annotations of the form //@ ...annotation.... Such an annotation is entirely equivalent to /*@ ...annotation... @*/.

Notice that the requires clause, the ensures clause, and the unwind ensures clause must be in separate annotations.