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

// Standard library: byte buffer contracts
module std.bytes

contract from_string {
    input(s: String)
    output(result: Bytes)
    ensures { result.length() >= 0 }
    effects { pure }
}

contract to_string {
    input(data: Bytes)
    output(result: String)
    effects { pure }
}

contract bytes_length {
    input(data: Bytes)
    output(result: Nat)
    ensures { result >= 0 }
    effects { pure }
}

contract slice {
    input(data: Bytes, start: Nat, end: Nat)
    output(result: Bytes)
    requires { start <= end }
    requires { end <= data.length() }
    effects { pure }
}

contract concat {
    input(a: Bytes, b: Bytes)
    output(result: Bytes)
    effects { pure }
}

contract starts_with {
    input(data: Bytes, prefix: Bytes)
    output(result: Bool)
    effects { pure }
}

contract byte_at {
    input(data: Bytes, index: Nat)
    output(result: Nat)
    requires { index < data.length() }
    effects { pure }
}