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
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
/*
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;
}
|
