anodized 0.5.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

use anodized::arithmetic::int;
use anodized::spec;

#[spec(
    requires: n > 0,
    ensures: *output == 1,
)]
pub fn collatz(mut n: int) -> int {
    while n > 1 {
        n = f(&n);
    }
    n
}

fn f(n: &int) -> int {
    if n % 2 == 0 { n / 2 } else { 3 * n + 1 }
}