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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91

The change from v0.2.0 to v0.3.0 includes some syntax changes to macro attributes. Here is what you should change in your code:

# Recursive definition

Old recursive definition looked like this:

```
#[define_rec]
fn add(..) -> {
    ..
}
```

Update to this:

```
#[define]
#[recursive]
fn add(..) -> {
    ..
}
```

# Annotations and AssumeFor

Old function-axiom looked like this:

```
#[assume_for(union)]
fn union_def() -> bool {
    |a: MySet, b: MySet|
    |c: MySet|
    forall(|e: u32| {
        member(e,c) == (member(e,a) || member(e,b))
}
```

Update to this:

```
#[assume(union(a, b) => c)]
fn union_def() -> bool {
    forall(|e: u32| {
        member(e,c) == (member(e,a) || member(e,b))
}
```

Old annotation looked like this:

```
#[annotate(union)]
fn union_def() -> bool {
    |a: MySet, b: MySet|
    |c: MySet|
    forall(|e: u32| {
        member(e,c) == (member(e,a) || member(e,b))
}
```

Update to this:

```
#[annotate(union(a, b) => c)]
fn union_def() -> bool {
    forall(|e: u32| {
        member(e,c) == (member(e,a) || member(e,b))
}
```

# Polymorphism

Old polymorphic assume looks like this:

```
#[assume((HashSet<E>, E))]
fn empty_no_member<E: Eq + Hash>() -> bool {
    forall(|e: E| !member_poly::<E>(e, empty_poly::<E>()))
}
```

Update to this:

```
#[assume]
#[for_type(HashSet<E> => <E>)]
fn empty_no_member<E: Eq + Hash>() -> bool {
    forall(|e: E| !member_poly::<E>(e, empty_poly::<E>()))
}
```

You can use multiple `for_type` lines.