Attribute Macro maintains 

#[maintains]

Allows specifying both a pre- and post-condition in a single statement.

Expects an expression in either the form of a method or function call Arguments to the call can be prefixed with mut to indicate that they are mutable borrows.

Generates a requires and ensures clause in the shape of the input expression, with mut replaced by * in the requires and ^ in the ensures.