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
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

use anodized::spec;

#[spec(
    ensures: [
        seq.iter().any(|elem| elem == output),
        seq.iter().all(|elem| elem <= output),
    ],
)]
pub fn find_maximum(seq: &[u8]) -> u8 {
    let mut max = 0;

    #[spec(
        maintains: seq[0..i].iter().all(|elem| elem <= &max),
    )]
    for i in 0..seq.len() {
        if seq[i] > max {
            max = seq[i]
        }
    }

    max
}

#[spec(
    requires: seq.is_sorted(),
    ensures: [
        *output <= seq.len(),
        seq[0..*output].iter().all(|item| item < value),
        seq[*output..].iter().all(|item| item >= value),
    ],
)]
pub fn find_insert_position<T: Ord>(seq: &[T], value: &T) -> usize {
    let mut i = 0;

    #[spec(
        maintains: seq[0..i].iter().all(|item| item < value),
        decreases: seq.len() - i,
    )]
    while i < seq.len() && seq[i] < *value {
        i += 1;
    }

    i
}