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
module 0x42::TestSpecBlock {
fun simple1(x: u64, y: u64) {
if (!(x > y)) abort 1;
spec {
assert x > y;
}
}
fun simple2(x: u64) {
let y: u64;
y = x + 1;
spec {
assert x == y - 1;
}
}
fun simple3(x: u64, y: u64) {
spec {
assume x > y;
assert x >= y;
}
}
fun simple4(x: u64, y: u64) {
let z: u64;
z = x + y;
spec {
assume x > y;
assert z > 2*y;
}
}
fun looping(x: u64): u64 {
spec { assume x <= 10; };
while (x < 10) {
spec { assume x < 10; };
x = x + 1;
};
spec { assert x == 10; };
x
}
}