Crate contracts

A crate implementing "Design by Contract" via procedural macros.

This crate is heavily inspired by the libhoare compiler plugin.

The main use of this crate is to annotate functions and methods using "contracts" in the form of pre-conditions, postconditions and invariants.

Each "contract" annotation that is violated will cause an assertion failure.

The attributes use "function call form" and can contain 1 or more conditions to check. If the last argument to an attribute is a string constant it will be inserted into the assertion message.

#[pre(x > 0, "x must be in the valid input range")]
#[post(ret.map(|s| s * s == x).unwrap_or(true))]
fn integer_sqrt(x: u64) -> Option<u64> {
   // ...
}

Attribute Macros

invariant	Invariants are conditions that have to be maintained at the "interface boundaries".
post	Post-conditions are checked after the function body is run.
pre	Pre-conditions are checked before the function body is run.