anodized 0.6.0

A common specification layer for Rust
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

use anodized::spec;

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

#[cfg(all(anodized_print, anodized_panic))]
#[test]
#[should_panic(expected = "postcondition failed:\
\n    a <= b")]
fn sort_fail_postcondition() {
    sort_pair((2, 5));
}