contracts 0.2.0

Design-by-contract attributes
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

/* This Source Code Form is subject to the terms of the Mozilla Public
 * License, v. 2.0. If a copy of the MPL was not distributed with this
 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */

//! Testing of simple functions.

use contracts::*;
use quickcheck_macros::quickcheck;

#[test]
fn test_a_thing() {
    #[pre(x > 10, x < 20, "x must be in valid range")]
    #[post(ret > x, "result will be bigger than input")]
    fn a(x: usize) -> usize {
        x + 1
    }

    a(15);
}

#[quickcheck]
fn test_sort(input: Vec<usize>) {
    fn is_sorted(input: &[usize]) -> bool {
        if input.len() < 2 {
            return true;
        }

        for i in 1..input.len() {
            if input[i - 1] > input[i] {
                return false;
            }
        }

        true
    }

    #[post(ret.len() == input.len())]
    #[test_post(is_sorted(&ret))]
    fn sort(input: &[usize]) -> Vec<usize> {
        let mut vec = input.to_owned();

        vec.sort();

        vec
    }

    sort(&input);
}

#[test]
fn test_invariant() {
    #[invariant(*val <= 10)]
    fn add_to_10(val: &mut usize) {
        if *val >= 10 {
            return;
        }
        *val += 1;
    }

    let mut val = 8;

    add_to_10(&mut val);
    add_to_10(&mut val);
    add_to_10(&mut val);
    add_to_10(&mut val);
    add_to_10(&mut val);
}