Attribute Macro contracts::ensures

#[ensures]

Post-conditions are checked after the function body is run.

The result of the function call is accessible in conditions using the ret identifier.

A “pseudo-function” named old can be used to evaluate expressions in a context prior to function execution. This function takes only a single argument and the result of it will be stored in a variable before the function is called. Because of this, handling references might require special care.

Examples

#[ensures(ret > x)]
fn incr(x: usize) -> usize {
    x + 1
}

#[ensures(*x == old(*x) + 1, "x is incremented")]
fn incr(x: &mut usize) {
    *x += 1;
}