[][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.


#[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


A "contract_trait" is a trait which ensures all implementors respect all provided contracts.


Same as invariant, but uses debug_assert!.


Same as post, but uses debug_assert!.


Same as pre, but uses debug_assert!.


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


Post-conditions are checked after the function body is run.


Pre-conditions are checked before the function body is run.


Same as invariant, but is only enabled in #[cfg(test)] environments.


Same as post, but is only enabled in #[cfg(test)] environments.


Same as pre, but is only enabled in #[cfg(test)] environments.