summaryrefslogtreecommitdiff
path: root/Test/dafny0/MultiDimArray.dfy
blob: ba5dc9da4b2304d2552c9c687ce19ae7fe146c7b (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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
class A {
  // all of the following array types are allowed
  var a: array<int>;
  var b: array  <bool>;
  var c: array <A>;
  var d: array1 <A>;  // this is a synonym for array<A>
  var e: array2 <A>;
  var f: array3 <A>;
  var g: array300 <A>;
  var h: array3000 <array2<int>>;

  method M0()
    requires a != null && b != null;
    modifies a;
  {
    if (5 <= a.Length && a.Length <= b.Length) {
      var x := b[2];
      var y := a[1];
      var z := a[2];
      a[2] := a[2] + 1;
      assert x == b[2];
      assert y == a[1];
      assert z == a[2] - 1;
    }
  }

  method M1()
    requires a != null && d != null;
    modifies a;
  {
    if (5 <= a.Length && a.Length <= d.Length) {
      var x := d[2];
      var y := a[1];
      var z := a[2];
      a[2] := a[2] + 1;
      assert y == a[1];
      assert z == a[2] - 1;
      assert x == d[2];  // error: a and d may be equal
    }
  }

  method M2(i: int, j: int, k: int, val: A)
    requires f != null;
    requires 0 <= i && i < f.Length0;
    requires 0 <= j && j < f.Length1;
    requires 0 <= k && k < f.Length2;
    modifies f;
  {
    if (*) {
      if (k < f.Length0) {
        var save := f[k,j,k];
        f[i,j,k] := val;
        assert save == f[k,j,k];  // error: k and i may be equal
      }
    } else if (k < f.Length0 && k != i) {
      if (k < f.Length0) {
        var save := f[k,j,k];
        f[i,j,k] := val;
        assert save == f[k,j,k];  // fine
      }
    }
  }

  method M3(i: int, j: int, k: int)
    requires f != null;
    requires 0 <= i && i < f.Length0;
    requires 0 <= j && j < f.Length1;
    requires 0 <= k && k < f.Length2;
    modifies f;
    decreases i;
  {
    if (i != 0) {
      var z := new A[2,3,5];  // first three primes (nice!)
      var s := z[1,2,4];  // first three powers of 2 (tra-la-la)
      var some: A;
      f[i,j,k] := some;
      call M3(i-1, j, k);
      assert s == z[1,2,4];
      if (*) {
        assert f[i,j,k] == some;  // error: the recursive call may have modified any element in 'f'
      }
    }
  }

  method M4(a: array2<bool>) returns (k: int)
    requires a != null;
    ensures 0 <= k;
  {
    k := a.Length0 + a.Length1;
  }
}