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
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83

use anodized::spec;

#[spec]
pub trait TestTrait {
    /// Returns a current value
    fn current(&self) -> i32;

    /// Has no default
    #[spec(
        requires: x > 0,
        captures: self.current() as old_val,
        ensures: *output > old_val,
    )]
    fn add_to(&self, x: i32) -> i32;

    /// Has a default
    #[spec(
        requires: x > 0,
        captures: self.current() as old_val,
        ensures: *output > old_val,
    )]
    fn mul_by(&self, x: i32) -> i32 {
        x * 2
    }
}

struct TestStruct(i32);

#[spec]
impl TestTrait for TestStruct {
    fn current(&self) -> i32 {
        self.0
    }

    fn add_to(&self, x: i32) -> i32 {
        x + self.current()
    }

    #[inline(never)]
    fn mul_by(&self, x: i32) -> i32 {
        x * self.0
    }
}

struct TestStructConst;

#[spec]
impl TestTrait for TestStructConst {
    fn current(&self) -> i32 {
        0
    }

    fn add_to(&self, x: i32) -> i32 {
        x + self.current()
    }
}

#[test]
fn should_succeed() {
    let test = TestStruct(3);
    assert_eq!(test.add_to(500), 503);
    assert_eq!(test.mul_by(500), 1500);

    let test = TestStructConst;
    assert_eq!(test.add_to(500), 500);
    assert_eq!(test.mul_by(500), 1000);
}

#[cfg(feature = "runtime-check-and-panic")]
#[test]
#[should_panic(expected = "Precondition failed: x > 0")]
fn should_fail_add_to() {
    let test = TestStruct(3);
    assert_eq!(test.add_to(0), 3);
}

#[cfg(feature = "runtime-check-and-panic")]
#[test]
#[should_panic(expected = "Postcondition failed: | output | * output > old_val")]
fn should_fail_negative_mul_by() {
    let test = TestStruct(-3);
    assert_eq!(test.mul_by(1), 3);
}