Attribute Macro contracts::contract_trait

#[contract_trait]

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

When this attribute is applied to a trait definition, the trait gets modified so that all invocations of methods are checked.

When this attribute is applied to an impl Trait for Type item, the implementation gets modified so it matches the trait definition.

When the #[contract_trait] is not applied to either the trait or an impl it will cause compile errors.

Example

#[contract_trait]
trait MyRandom {
    #[pre(min < max)]
    #[post(min <= ret, ret <= max)]
    fn gen(min: f64, max: f64) -> f64;
}

// Not a very useful random number generator, but a valid one!
struct AlwaysMax;

#[contract_trait]
impl MyRandom for AlwaysMax {
    fn gen(min: f64, max: f64) -> f64 {
        max
    }
}