[−][src]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, post-conditions 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.

Example

#[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> {
   // ...
}

Feature flags

Following feature flags are available:

disable_contracts - disables all checks and assertions.
override_debug - changes all contracts (except test_ ones) into debug_* versions
override_log - changes all contracts (except test_ ones) into a log::error!() call if the condition is violated. No abortion happens.

Attribute Macros

contract_trait	A "contract_trait" is a trait which ensures all implementors respect all provided contracts.
debug_invariant	Same as `invariant`, but uses `debug_assert!`.
debug_post	Same as `post`, but uses `debug_assert!`.
debug_pre	Same as `pre`, but uses `debug_assert!`.
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.
test_invariant	Same as `invariant`, but is only enabled in `#[cfg(test)]` environments.
test_post	Same as `post`, but is only enabled in `#[cfg(test)]` environments.
test_pre	Same as `pre`, but is only enabled in `#[cfg(test)]` environments.