Spec fn signature

The general form of a spec function signature takes the form:

spec fn function_name generics?(args...) -> return_type?
    where_clause?
    recommends_clause?
    decreases_clause?

The recommends clause

The recommends clauses is a “soft precondition”, which is sometimes checked for the sake of diagnostics, but is not a hard requirement for the function to be well-defined.

See this guide page for motivation and overview.

The decreases clause

The decreases clause is used to ensure that recursive definitions are well-formed. Note that if the decreases clauses has a when-subclause, it will restrict the function definition to the domain.

See the reference page for decreases for more information, or see the guide page on recursive functions for motivation and overview.