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

use anodized::spec;

#[spec(
    requires: x.is_finite(),
    ensures: output + output == x,
)]
async fn async_half(x: f32) -> f32 {
    todo!()
}

#[test]
fn async_function_compiles() {
    let future = async_half(5.0);

    fn is_future<T: core::future::Future>(_: &T) {}
    is_future(&future);
}