assura-stdlib 0.1.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
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76

// Standard library: string contracts
module std.string

contract string_length {
    input(s: String)
    output(result: Nat)
    ensures { result >= 0 }
    effects { pure }
}

contract substring {
    input(s: String, start: Nat, end: Nat)
    output(result: String)
    requires { start <= end }
    effects { pure }
}

contract contains {
    input(haystack: String, needle: String)
    output(result: Bool)
    effects { pure }
}

contract starts_with {
    input(s: String, prefix: String)
    output(result: Bool)
    effects { pure }
}

contract ends_with {
    input(s: String, suffix: String)
    output(result: Bool)
    effects { pure }
}

contract trim {
    input(s: String)
    output(result: String)
    effects { pure }
}

contract to_uppercase {
    input(s: String)
    output(result: String)
    effects { pure }
}

contract to_lowercase {
    input(s: String)
    output(result: String)
    effects { pure }
}

contract replace {
    input(s: String, from: String, to: String)
    output(result: String)
    effects { pure }
}

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

contract index_of {
    input(s: String, needle: String)
    output(result: Int)
    effects { pure }
}

contract is_empty {
    input(s: String)
    output(result: Bool)
    effects { pure }
}