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 }