assura-stdlib 0.4.0

Assura standard library contracts and prelude types
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

// Standard library: time contracts
module std.time

contract now_millis {
    output(result: Nat)
    ensures { result >= 0 }
    effects { time }
}

contract elapsed {
    input(start: Nat, end: Nat)
    output(result: Nat)
    requires { end >= start }
    effects { pure }
}

contract sleep_millis {
    input(millis: Nat)
    requires { millis > 0 }
    effects { time }
}