Macro adhesion::contract

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);