Exec fn signature #

The general form of an exec function signature takes the form:

V@[exec_fn_item] ::=
    R@[visibility]? exec? fn R@[function_name] R@[generics]?(R@[args...]) ( -> V@[exec_return_type] )?
        R@[where_clause]?
        V@[requires_clause]?
        V@[ensures_clause]?
        V@[returns_clause]?
        V@[invariants_clause]?
        V@[unwind_clause]?

V@[exec_return_type]       ::= V@[exec_return_type_named] | V@[exec_return_type_anon]
V@[exec_return_type_named] ::= ( R@[pattern] : R@[type] )
V@[exec_return_type_anon]  ::= R@[type]

Function specification #

The elements of the function specification are given by the signature clauses.

The precondition. The V@[requires_clause] is the precondition.

The postcondition. The V@[ensures_clause] and the V@[returns_clause] together form the postcondition.

The invariants. The V@[invariants_clause] specifies what invariants can be opened by the function. For exec functions, the default is opens_invariants any. See this page for more details.

Unwinding. The V@[unwind_clause] specifies whether the function might exit "abnormally" by unwinding, and under what conditions that can happen. See this page for more details.

Function arguments #

All arguments and return values need to have exec mode. To embed ghost/tracked variables into the signature, use the Tracked and Ghost types.

See here for more information.