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

use anodized::spec;

#[spec(
    // Should fail: closure has 2 arguments
    ensures: |x, y| x > 0,
)]
fn returns_positive() -> i32 {
    42
}

#[spec(
    // Should fail: closure has 0 arguments
    ensures: || true,
)]
fn returns_something() -> i32 {
    42
}

fn main() {}