Attribute Macro contracts::contract_trait
source · [−]#[contract_trait]
Expand description
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 {
#[requires(min < max)]
#[ensures(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
}
}