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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
/*
Rustan Leino, 5 Oct 2011
COST Verification Competition, Challenge 3: Two equal elements
http://foveoos2011.cost-ic0701.org/verification-competition
Given: An integer array a of length n+2 with n>=2. It is known that at
least two values stored in the array appear twice (i.e., there are at
least two duplets).
Implement and verify a program finding such two values.
You may assume that the array contains values between 0 and n-1.
*/
// Remarks:
// The implementation of method 'Search' takes one pass through the elements of
// the given array. To keep track of what it has seen, it allocates an array as
// temporary storage--I imagine that this is what the competition designers
// had in mind, since the problem description says one can assume the values
// of the given array to lie in the range 0..n.
// To keep track of whether it already has found one duplicate, the method
// sets the output variables p and q as follows:
// p != q - no duplicates found yet
// p == q - one duplicate found so far, namely the value stored in p and q
// Note, the loop invariant does not need to say anything about the state
// of two duplicates having been found, because when the second duplicate is
// found, the method returns.
// What needs to be human-trusted about this program is the specification of
// 'Search'. The specification straightforwardly lists the assumptions stated
// in the problem description, including the given fact that the array contains
// (at least) two distinct elements that each occurs (at least) twice. To
// trust the specification of 'Search', a human also needs to trust the definition
// of 'IsDuplicate' and its auxiliary function 'IsPrefixDuplicate'.
// 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 11 seconds)
// without further human intervention.
function IsDuplicate(a: array<int>, p: int): bool
requires a != null;
reads a;
{
IsPrefixDuplicate(a, a.Length, p)
}
function IsPrefixDuplicate(a: array<int>, k: int, p: int): bool
requires a != null && 0 <= k <= a.Length;
reads a;
{
exists i,j :: 0 <= i < j < k && a[i] == a[j] == p
}
method Search(a: array<int>) returns (p: int, q: int)
requires a != null && 4 <= a.Length;
requires exists p,q :: p != q && IsDuplicate(a, p) && IsDuplicate(a, q); // two distinct duplicates exist
requires forall i :: 0 <= i < a.Length ==> 0 <= a[i] < a.Length - 2; // the elements of "a" in the range [0.. a.Length-2]
ensures p != q && IsDuplicate(a, p) && IsDuplicate(a, q);
{
// allocate an array "d" and initialize its elements to -1.
var d := new int[a.Length-2];
var i := 0;
while (i < d.Length)
invariant 0 <= i <= d.Length && forall j :: 0 <= j < i ==> d[j] == -1;
{
d[i], i := -1, i+1;
}
i, p, q := 0, 0, 1;
while (true)
invariant 0 <= i < a.Length;
invariant forall j :: 0 <= j < d.Length ==>
(d[j] == -1 && forall k :: 0 <= k < i ==> a[k] != j) ||
(0 <= d[j] < i && a[d[j]] == j);
invariant p == q ==> IsDuplicate(a, p);
invariant forall k :: 0 <= k < i && IsPrefixDuplicate(a, i, a[k]) ==> p == q == a[k];
decreases a.Length - i;
{
var k := d[a[i]];
assert k < i; // note, this assertion is really for human consumption; it is not needed by the verifier, and it does not change the performance of the verifier
if (k == -1) {
// a[i] does not exist in a[..i]
d[a[i]] := i;
} else {
// we have encountered a duplicate
assert a[i] == a[k] && IsDuplicate(a, a[i]); // note, this assertion is really for human consumption; it is not needed by the verifier, and it does not change the performance of the verifier
if (p != q) {
// this is the first duplicate encountered
p, q := a[i], a[i];
} else if (p == a[i]) {
// this is another copy of the same duplicate we have seen before
} else {
// this is the second duplicate
q := a[i];
return;
}
}
i := i + 1;
}
}
|
