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 (requires), post-conditions (ensures) 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

#[requires(x > 0, "x must be in the valid input range")]
#[ensures(ret.is_some() -> ret.unwrap() * ret.unwrap() == x)]
fn integer_sqrt(x: u64) -> Option<u64> {
   // ...
}

pub struct Library {
    available: HashSet<String>,
    lent: HashSet<String>,
}

impl Library {
    fn book_exists(&self, book_id: &str) -> bool {
        self.available.contains(book_id)
            || self.lent.contains(book_id)
    }

    #[debug_requires(!self.book_exists(book_id), "Book IDs are unique")]
    #[debug_ensures(self.available.contains(book_id), "Book now available")]
    #[ensures(self.available.len() == old(self.available.len()) + 1)]
    #[ensures(self.lent.len() == old(self.lent.len()), "No lent change")]
    pub fn add_book(&mut self, book_id: &str) {
        self.available.insert(book_id.to_string());
    }

    #[debug_requires(self.book_exists(book_id))]
    #[ensures(ret -> self.available.len() == old(self.available.len()) - 1)]
    #[ensures(ret -> self.lent.len() == old(self.lent.len()) + 1)]
    #[debug_ensures(ret -> self.lent.contains(book_id))]
    #[debug_ensures(!ret -> self.lent.contains(book_id), "Book already lent")]
    pub fn lend(&mut self, book_id: &str) -> bool {
        if self.available.contains(book_id) {
            self.available.remove(book_id);
            self.lent.insert(book_id.to_string());
            true
        } else {
            false
        }
    }

    #[debug_requires(self.lent.contains(book_id), "Can't return a non-lent book")]
    #[ensures(self.lent.len() == old(self.lent.len()) - 1)]
    #[ensures(self.available.len() == old(self.available.len()) + 1)]
    #[debug_ensures(!self.lent.contains(book_id))]
    #[debug_ensures(self.available.contains(book_id), "Book available again")]
    pub fn return_book(&mut self, book_id: &str) {
        self.lent.remove(book_id);
        self.available.insert(book_id.to_string());
    }
}

Attributes

This crate exposes the requires, ensures and invariant attributes.

• requires are checked before a function/method is executed.
• ensures are checked after a function/method ran to completion
• invariants are checked both before and after a function/method ran.

Additionally, all those attributes have versions with different “modes”. See the Modes section below.

For traits and trait impls the contract_trait attribute can be used.

Pseudo-functions and operators

old() function

One unique feature that this crate provides is an old() pseudo-function which allows to perform checks using a value of a parameter before the function call happened. This is only available in ensures attributes.

#[ensures(*x == old(*x) + 1, "after the call `x` was incremented")]
fn incr(x: &mut usize) {
    *x += 1;
}

-> operator

For more complex functions it can be useful to express behaviour using logical implication. Because Rust does not feature an operator for implication, this crate adds this operator for use in attributes.

#[ensures(person_name.is_some() -> ret.contains(person_name.unwrap()))]
fn geeting(person_name: Option<&str>) -> String {
    let mut s = String::from("Hello");
    if let Some(name) = person_name {
        s.push(' ');
        s.push_str(name);
    }
    s.push('!');
    s
}

This operator is right-associative.

Note: Because of the design of syn, it is tricky to add custom operators to be parsed, so this crate performs a rewrite of the TokenStream instead. The rewrite works by separating the expression into a part that’s left of the -> operator and the rest on the right side. This means that if a -> b { c } else { d } will not generate the expected code. Explicit grouping using parenthesis or curly-brackets can be used to avoid this.

Modes

All the attributes (requires, ensures, invariant) have debug_* and test_* versions.

• debug_requires/debug_ensures/debug_invariant use debug_assert! internally rather than assert!

• test_requires/test_ensures/test_invariant guard the assert! with an if cfg!(test). This should mostly be used for stating equivalence to “slow but obviously correct” alternative implementations or checks.

  For example, a merge-sort implementation might look like this

  #[test_ensures(is_sorted(input))]
  fn merge_sort<T: Ord + Copy>(input: &mut [T]) {
      // ...
  }

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.
• mirai_assertions - instead of regular assert! style macros, emit macros used by the MIRAI static analyzer.

Attribute Macros

contract_trait

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

debug_ensures

Same as ensures, but uses debug_assert!.

debug_invariant

Same as invariant, but uses debug_assert!.

debug_requires

Same as requires, but uses debug_assert!.

ensures

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

invariant

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

requires

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

test_ensures

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

test_invariant

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

test_requires

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