ravencheck 0.5.0

Decidable verification of Rust code using relational abstraction.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

#[crate::check_module(crate)]
#[allow(dead_code)]
mod match_exclusion {
    #[define]
    enum Opt<T> {
        Some(T),
        None,
    }

    #[verify]
    fn not_some_and_none<T>(v: Opt<T>) -> bool {
        let some = exists(|t: T| v == Opt::<T>::Some(t));
        let none = v == Opt::<T>::None;
        !(some && none)
    }

    // This is not currently enforced by the constructor axioms.
    #[falsify]
    fn some_or_none<T>(v: Opt<T>) -> bool {
        let some = exists(|t: T| v == Opt::<T>::Some(t));
        let none = v == Opt::<T>::None;
        (some || none)
    }
}