[−][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 (excepttest_
ones) intodebug_*
versionsoverride_log
- changes all contracts (excepttest_
ones) into alog::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 |
debug_post | Same as |
debug_pre | Same as |
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 |
test_post | Same as |
test_pre | Same as |