anodized 0.4.0

An ecosystem for correct Rust based on lightweight specification annotations
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

use anodized::spec;

#[spec(
    binds: (a, b),
    ensures: [
        a <= b,
        (*a, *b) == pair || (*b, *a) == pair,
    ],
)]
fn sort_pair(pair: (i32, i32)) -> (i32, i32) {
    // Deliberately wrong implementation to break the spec.
    pair
}

#[cfg(feature = "runtime-check-and-panic")]
#[test]
#[should_panic(expected = "Postcondition failed: | (a, b) | a <= b")]
fn sort_fail_postcondition() {
    sort_pair((5, 2));
}