Test/dafny2/Intervals.dfy


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

// The RoundDown and RoundUp methods in this file are the ones in the Boogie
// implementation Source/AbsInt/IntervalDomain.cs.

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