extern_spec_T__slice_T_binary_search

creusot_contracts::std::slice

Function extern_spec_T__slice_T_binary_search 

Source 
pub fn extern_spec_T__slice_T_binary_search<T>(
    self_: &[T],
    x: &T,
) -> Result<usize, usize>
where
    T: Ord + DeepModel,
    T::DeepModelTy: OrdLogic,
Expand description

extern spec for slice<T>::binary_search

This is not a real function: its only use is for documentation.

requires 

self.deep_model().sorted()

ensures

forall<i:usize> result == Ok(i) ==>
            i@ < self@.len() && (*self).deep_model()[i@] == x.deep_model()

ensures

forall<i:usize> result == Err(i) ==> i@ <= self@.len() &&
            forall<j> 0 <= j && j < self@.len() ==> self.deep_model()[j] != x.deep_model()

ensures

forall<i:usize> result == Err(i) ==>
            forall<j:usize> j < i ==> self.deep_model()[j@] < x.deep_model()

ensures

forall<i:usize> result == Err(i) ==>
            forall<j:usize> i <= j && j@ < self@.len() ==> x.deep_model() < self.deep_model()[j@]