anodized 0.5.1

A common specification layer for Rust
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

#![no_main]

use anodized::spec;

#[spec(
    requires: self.x > 0.0,
    maintains: self.x != self.y,
    captures: self.x as old_x,
    binds: ret_val,
    ensures: self.y > 0.0,
)]
struct Point {
    x: f32,
    y: f32,
}