automation-structures 0.1.1

Reusable, formally specified building blocks for composing automation systems.
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

//! Canonical Counter connective relations for retained integer progress.

use vstd::prelude::*;

verus! {

/// A retained count remains nonnegative.
pub open spec fn nonnegative(value: int) -> bool {
    0 <= value
}

/// A retained generation or occurrence count is present and nonzero.
pub open spec fn positive(value: int) -> bool {
    &&& nonnegative(value)
    &&& value > 0
}

/// One occurrence advances retained progress by one.
pub open spec fn increment(pre: int, post: int) -> bool {
    post == pre + 1
}

/// A counted occurrence that leaves its retained count unchanged is rejected.
pub proof fn stalled_increment_rejected(pre: int)
    ensures !increment(pre, pre),
{
}

/// An unselected occurrence preserves retained progress.
pub open spec fn stutter(pre: int, post: int) -> bool {
    post == pre
}

/// One selected occurrence decrements while every unselected occurrence stutters.
pub open spec fn decrement_if(pre: int, post: int, selected: bool) -> bool {
    post == pre - if selected { 1int } else { 0int }
}

/// A selected decrement has available credit and preserves nonnegativity.
pub open spec fn guarded_decrement_if(pre: int, post: int, selected: bool) -> bool {
    &&& nonnegative(pre)
    &&& decrement_if(pre, post, selected)
    &&& nonnegative(post)
    &&& (selected ==> 0 < pre)
}

}