Attribute Macro ensures

Source
#[ensures]