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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
|
class Math {
ghost var Repr: set<object>;
function Valid_repr(): bool
reads *;
{
this in Repr &&
null !in Repr
}
function Valid_self(): bool
reads *;
{
Valid_repr() &&
true
}
function Valid(): bool
reads *;
{
this.Valid_self() &&
true
}
method Abs(a: int) returns (ret: int)
requires Valid();
ensures fresh(Repr - old(Repr));
ensures Valid();
ensures ret in {a, -a};
ensures ret >= 0;
{
if (a >= 0) {
ret := a;
} else {
ret := -a;
}
}
method Min2(a: int, b: int) returns (ret: int)
requires Valid();
ensures fresh(Repr - old(Repr));
ensures Valid();
ensures a < b ==> ret == a;
ensures a >= b ==> ret == b;
{
if (a < b) {
ret := a;
} else {
ret := b;
}
}
method Min3Sum(a: int, b: int, c: int) returns (ret: int)
requires Valid();
ensures fresh(Repr - old(Repr));
ensures Valid();
ensures ret in {a + b, a + c, b + c};
ensures ret <= a + b;
ensures ret <= a + c;
ensures ret <= b + c;
{
if (a + b <= a + c && a + b <= b + c) {
ret := a + b;
} else {
if (b + c <= a + c) {
ret := b + c;
} else {
ret := a + c;
}
}
}
method Min4(a: int, b: int, c: int, d: int) returns (ret: int)
requires Valid();
ensures fresh(Repr - old(Repr));
ensures Valid();
ensures ret in {a, b, c, d};
ensures ret <= a;
ensures ret <= b;
ensures ret <= c;
ensures ret <= d;
{
if ((a <= b && a <= c) && a <= d) {
ret := a;
} else {
if (d <= b && d <= c) {
ret := d;
} else {
if (c <= b) {
ret := c;
} else {
ret := b;
}
}
}
}
}
|
