Attribute Macro contracts::requires

#[requires]

Pre-conditions are checked before the function body is run.

Example

#[requires(elems.len() >= 1)]
fn max<T: Ord + Copy>(elems: &[T]) -> T {
   // ...
}