summaryrefslogtreecommitdiff
path: root/Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy
blob: f67d78704d1dafc62b9094f91ffc4727c6b87dbb (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
/*
Rustan Leino, 5 Oct 2011

COST Verification Competition, Challenge 1: Maximum in an array
http://foveoos2011.cost-ic0701.org/verification-competition

Given: A non-empty integer array a.

Verify that the index returned by the method max() given below points to
an element maximal in the array.

public class Max {
    public static int max(int[] a) {
        int x = 0;
        int y = a.length-1;

        while (x != y) {
            if (a[x] <= a[y]) x++;
                else y--;
        }
        return x;
    }
}
*/

// Remarks:

// The verification of the loop makes use of a local ghost variable 'm'.  To the
// verifier, this variable is like any other, but the Dafny compiler ignores it.
// In other words, ghost variables and ghost assignments (and specifications,
// for that matter) are included in the program just for the purpose of reasoning
// about the program, and they play no role at run time.

// The only thing that needs to be human-trusted about this program is the
// specification of 'max' (and, since verification challenge asked to prove
// something about a particular piece of code, that the body of 'max', minus
// the ghost constructs, is really that code).

// About Dafny:
// As always (when it is successful), Dafny verifies that the program does not
// cause any run-time errors (like array index bounds errors), that the program
// terminates, that expressions and functions are well defined, and that all
// specifications are satisfied.  The language prevents type errors by being type
// safe, prevents dangling pointers by not having an "address-of" or "deallocate"
// operation (which is accommodated at run time by a garbage collector), and
// prevents arithmetic overflow errors by using mathematical integers (which
// is accommodated at run time by using BigNum's).  By proving that programs
// terminate, Dafny proves that a program's time usage is finite, which implies
// that the program's space usage is finite too.  However, executing the
// program may fall short of your hopes if you don't have enough time or
// space; that is, the program may run out of space or may fail to terminate in
// your lifetime, because Dafny does not prove that the time or space needed by
// the program matches your execution environment.  The only input fed to
// the Dafny verifier/compiler is the program text below; Dafny then automatically
// verifies and compiles the program (for this program in less than 2 seconds)
// without further human intervention.

method max(a: array<int>) returns (x: int)
  requires a != null && a.Length != 0;
  ensures 0 <= x < a.Length;
  ensures forall i :: 0 <= i < a.Length ==> a[i] <= a[x];
{
  x := 0;
  var y := a.Length - 1;
  ghost var m := y;
  while (x != y)
    invariant 0 <= x <= y < a.Length;
    invariant m == x || m == y;
    invariant forall i :: 0 <= i < x ==> a[i] <= a[m];
    invariant forall i :: y < i < a.Length ==> a[i] <= a[m];
  {
    if (a[x] <= a[y]) {
      x := x + 1;  m := y;
    } else {
      y := y - 1;  m := x;
    }
  }
  return x;
}