Attribute Macro contracts::invariant

#[invariant]

Invariants are conditions that have to be maintained at the “interface boundaries”.

Invariants can be supplied to functions (and “methods”), as well as on impl blocks.

When applied to an impl-block all methods taking self (either by value or reference) will be checked for the invariant.

Example

On a function:

/// Update `num` to the next bigger even number.
#[invariant(*num % 2 == 0)]
fn advance_even(num: &mut usize) {
    *num += 2;
}

On an impl-block:

struct EvenAdder {
    count: usize,
}

#[invariant(self.count % 2 == 0)]
impl EvenAdder {
    pub fn tell(&self) -> usize {
        self.count
    }

    pub fn advance(&mut self) {
        self.count += 2;
    }
}