blob: ef40910e25e51dc63dc316d1249be496e6440e57 (
plain)
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
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// The RoundDown and RoundUp methods in this file are the ones in the Boogie
// implementation Source/AbsInt/IntervalDomain.cs.
class Rounding {
var thresholds: array<int>;
function Valid(): bool
reads this, thresholds;
{
thresholds != null &&
forall m,n :: 0 <= m < n < thresholds.Length ==> thresholds[m] <= thresholds[n]
}
method RoundDown(k: int) returns (r: int)
requires Valid();
ensures -1 <= r < thresholds.Length;
ensures forall m :: r < m < thresholds.Length ==> k < thresholds[m];
ensures 0 <= r ==> thresholds[r] <= k;
{
if (thresholds.Length == 0 || k < thresholds[0]) {
return -1;
}
var i, j := 0, thresholds.Length - 1;
while (i < j)
invariant 0 <= i <= j < thresholds.Length;
invariant thresholds[i] <= k;
invariant forall m :: j < m < thresholds.Length ==> k < thresholds[m];
{
var mid := i + (j - i + 1) / 2;
assert i < mid <= j;
if (thresholds[mid] <= k) {
i := mid;
} else {
j := mid - 1;
}
}
return i;
}
method RoundUp(k: int) returns (r: int)
requires Valid();
ensures 0 <= r <= thresholds.Length;
ensures forall m :: 0 <= m < r ==> thresholds[m] < k;
ensures r < thresholds.Length ==> k <= thresholds[r];
{
if (thresholds.Length == 0 || thresholds[thresholds.Length-1] < k) {
return thresholds.Length;
}
var i, j := 0, thresholds.Length - 1;
while (i < j)
invariant 0 <= i <= j < thresholds.Length;
invariant k <= thresholds[j];
invariant forall m :: 0 <= m < i ==> thresholds[m] < k;
{
var mid := i + (j - i) / 2;
assert i <= mid < j;
if (thresholds[mid] < k) {
i := mid + 1;
} else {
j := mid;
}
}
return i;
}
}
|
