Test/dafny0/ResolutionErrors.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

method UmmThisIsntGoingToWork()
{
   var a := new int [2];
   var b := new int [1];
   a[0] := 1;
   a[1] := -1;

   ghost var i := 0;
   while (i < 2)
      decreases *;  // error: not allowed on a ghost loop
      invariant i <= 2;
      invariant forall j :: 0 <= j && j < i ==> a[j] > 0;
   {
      i := 0;
   }
   assert a[1] == -1;  // ...for then this would incorrectly verify
   b[a[1]] := 0;
}

method M<T>(a: array3<T>, b: array<T>, m: int, n: int)
{
  // the following invalid expressions were once incorrectly resolved:
  var x := a[m, n];        // error
  var y := a[m];           // error
  var z := b[m, n, m, n];  // error
}