invariant

States a condition that must always hold for a class’s instances, or each time a loop tests its condition.

On a class (class Name invariant cond { … }) it is checked after new and whenever a pub method returns. On a while or for loop it is checked before the first iteration and after each one. Contextual: only a keyword in those headers.

class Account
    invariant self.balance >= 0, "no overdraft"
{
    balance: int,
}

fn main() {
    let i = 0;
    while i < 3
        invariant i <= 3
    {
        i = i + 1;
    }
}

See also#

• fn: Declares a function, a method, or (written in an expression) an anonymous function.
• let: Declares a mutable local variable.
• const: Declares a binding that cannot be reassigned: a local, a module constant, or a class field that is set only by new.
• static: Declares a module-level or class-level slot shared by the whole program, or a method without self.
• readonly: A read-only view of a value: nothing reachable through it can be changed.
• if: Runs a block when a bool condition is true.
• else: Introduces the branch of an if that runs when its condition is false (or its pattern does not match).
• while: Repeats a block while a bool condition is true.