Skip to main content

next_postcondition

vstd::string

Function next_postcondition 

Source 
pub broadcast proof fn next_postcondition<'a>(
    old_chars: &Chars<'a>,
    new_chars: &Chars<'a>,
    ret: Option<char>,
)
Expand description
requires
#[trigger] next_post(old_chars, new_chars, ret),
ensures
new_chars.obeys_prophetic_iter_laws() == old_chars.obeys_prophetic_iter_laws(),
new_chars.obeys_prophetic_iter_laws()
    ==> new_chars.will_return_none() == old_chars.will_return_none(),
new_chars.obeys_prophetic_iter_laws()
    ==> (old_chars.decrease() is Some <==> new_chars.decrease() is Some),
new_chars.obeys_prophetic_iter_laws()
    ==> ({
        if old_chars.remaining().len() > 0 {
            &&& new_chars.remaining() == old_chars.remaining().drop_first()
            &&& ret == Some(old_chars.remaining()[0])

        } else {
            new_chars.remaining() == old_chars.remaining() && ret == None
                && new_chars.will_return_none()
        }
    }),
new_chars.obeys_prophetic_iter_laws() && old_chars.remaining().len() > 0
    && new_chars.decrease() is Some
    ==> decreases_to!(old_chars.decrease() -> 0 => new_chars.decrease() -> 0),