Function vstd::pervasive::spec_affirm

source · 
pub closed spec fn spec_affirm(b: bool) -> bool
Expand description
recommends
b,

A tool to check one’s reasoning while writing complex spec functions. Not intended to be used as a mechanism for instantiating quantifiers, spec_affirm should be removed from spec functions once they are complete.

Example

#[spec(checked)] fn some_predicate(a: nat) -> bool {
    recommends(a < 100);
    if (a >= 50) {
        let _ = spec_affirm(50 <= a && a < 100);
        a >= 75
    } else {
        let _ = spec_affirm(a < 50);
        // let _ = spec_affirm(a < 40); would raise a recommends note here
        a < 25
    }
}