Macro adhesion::contract
[−]
[src]
macro_rules! contract { ( $(#[$attribute: meta])* fn $name: ident $args: tt $( -> $return_type: ty)* { $(#![$inner_attribute: meta])+ $($block_name: ident $(($param: ident))* { $($block_content: tt)* })* } ) => { ... }; ( $(#[$attribute: meta])* fn $name: ident $args: tt $( -> $return_type: ty)* { $($block_name: ident $(($param: ident))* { $($block_content: tt)* })* } ) => { ... }; }
Converts a fn
definition inside to be a contracted function, complete with invariant, pre-, and post-conditions.
No blocks in this macro are required, nor is any specific order required.
Examples
contract! { fn asdf(asda: bool, stuff: u64) -> bool { pre { assert!(stuff < 30, "pre-condition violation"); } body { asda } post(return_value) { assert!(return_value == (stuff % 3 == 0), "post-condition violation"); } invariant { assert!(stuff > 5, "invariant violation"); } } } assert_that!(asdf(true, 7), panics); // post failure assert_that!(asdf(true, 64), panics); // pre failure assert_that!(asdf(false, 3), panics); // invariant failure asdf(true, 6); asdf(false, 7); asdf(false, 11); asdf(true, 24);