[−][src]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 } }