Exec fn signature

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

fn function_name generics?(args...) -> return_type_and_name?
    where_clause?
    requires_clause?
    ensures_clause?
    returns_clause?
    invariants_clause?
    unwind_clause?

Function specification

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

The precondition. The requires_clause is the precondition.

The postcondition. The ensures_clause and the returns_clause together form the postcondition.

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

Unwinding. The 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.