Attribute Macro ensures 

#[ensures]

A post-condition of a function or trait item

The post-condition can refer to the result of the function as result by default, or by naming it explicitly; see example below.

The inside of a ensures may look like Rust code, but it is in fact pearlite.

See also the guide: requires and ensures.

Example

#[ensures(result@ == 1)]
#[ensures(|one| one@ == 1)] // Explicitly name the result variable `one`
fn foo() -> i32 { 1 }

Constants

Constants may also have ensures clauses:

#[ensures(C@ > 24)]
const C: usize = 42;

The #[ensures] clause must use the actual name of the constant, and not result.

The presence of #[ensures] hides the definition of the constant from the translation of callers, so that the given specification is the only fact known to callers about the constant.

By default, the body of the constant is inlined in the translation of callers. However, this is not possible if it exposes private fields. You must use #[ensures] in that case.