ravencheck 0.4.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
25
26
27
28
29
30
31
32
33
34
35

#[crate::check_module(crate)]
#[allow(dead_code)]
pub mod my_mod {
    use std::collections::HashSet;

    #[declare]
    #[derive(PartialEq, Eq, Clone)]
    pub struct Set(pub HashSet<u32>);

    #[declare]
    #[derive(PartialEq, Eq, Clone, Copy)]
    pub struct Elem(u32);

    #[declare]
    pub fn member(e: Elem, s: Set) -> bool {
        s.0.contains(&e.0)
    }

    #[assume]
    fn equal_or_distinguisher() -> bool {
        forall(|x:Set,y:Set| {
            x == y || exists(|e:Elem| member(e,x) !=  member(e,y))
        })
    }

    #[falsify]
    fn prop1() -> bool {
        forall(|a: Set, b: Set| a == b)
    }

    #[verify]
    fn prop2() -> bool {
        forall(|e: Elem, s: Set| member(e,s) == member(e,s))
    }
}