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
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
|
// RUN: %dafny /compile:3 /autoTriggers:1 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// Rustan Leino
// 12 April 2015
// VerifyThis 2015
// Problem 1 -- Relaxed Prefix
// The property IsRelaxedPrefix is defined in terms of an auxiliary function. The
// auxiliary function allows a given number (here, 1) of elements to be dropped from
// the pattern.
predicate IsRelaxedPrefix<T>(pat: seq<T>, a: seq<T>)
{
IsRelaxedPrefixAux(pat, a, 1)
}
// This predicate returns whether or not "pat", dropping up to "slack" elements, is
// a prefix of "a".
predicate IsRelaxedPrefixAux<T>(pat: seq<T>, a: seq<T>, slack: nat)
{
// if "pat" is the empty sequence, the property holds trivially, regardless of the slack
if pat == [] then true
// if both "pat" and "a" are nonempty and they agree on their first element, then the property
// holds iff it holds of their drop-1 suffixes
else if a != [] && pat[0] == a[0] then IsRelaxedPrefixAux(pat[1..], a[1..], slack)
// if either "a" is empty or "pat" and "a" disagree on their first element, then the property
// holds iff there's any slack left and the property holds after spending 1 slack unit and dropping
// the first element of the pattern
else slack > 0 && IsRelaxedPrefixAux(pat[1..], a, slack-1)
}
// Here is the corrected reference implementation. The specification says to return true iff
// "pat" is a relaxed prefix of "a".
method ComputeIsRelaxedPrefix<T(==)>(pat: seq<T>, a: seq<T>) returns (b: bool)
ensures b == IsRelaxedPrefix(pat, a)
{
// This implementation is the given reference implementation but with two corrections. One
// correction is the out-of-bounds error in the indexing of "a". This is corrected here by
// strengthening the guard of the while loop. The other correction is that after the loop, the
// property still holds if "a" has been exhausted but the number of elements left to inspect in
// the pattern does not exceed the number of elements we are still allowed to drop. (There are
// other ways the given reference implementation could have been fixed as well.)
ghost var B := IsRelaxedPrefixAux(pat, a, 1); // the answer we want
var shift, i := 0, 0;
while i < |pat| && i-shift < |a|
invariant 0 <= i <= |pat| && i-shift <= |a|
invariant 0 <= shift <= i
invariant IsRelaxedPrefixAux(pat[i..], a[i-shift..], 1-shift) == B
{
if pat[i] != a[i-shift] {
if shift == 0 {
shift := 1;
} else {
return false;
}
}
i := i + 1;
}
return i - shift <= |pat| <= i - shift + 1;
}
method Main()
{
var a := [1,3,2,3];
var b := ComputeIsRelaxedPrefix([1,3], a);
print b, "\n";
b := ComputeIsRelaxedPrefix([1,2,3], a);
print b, "\n";
b := ComputeIsRelaxedPrefix([1,2,4], a);
print b, "\n";
}
// Here is an alternative definition of IsRelaxedPrefix. Perhaps this definition more obviously
// follows the English description of "relaxed prefix" given in the problem statement.
predicate IRP_Alt<T>(pat: seq<T>, a: seq<T>)
{
// "pat" is a relaxed prefix of "a"
// if "pat" is an actual prefix of "a"
pat <= a ||
// or if after dropping one element from "pat", namely the one at an index "k", then the result
// is a prefix of "a"
exists k :: 0 <= k < |pat| && pat[..k] + pat[k+1..] <= a
}
// We prove that the alternate definition is the same as the one given above.
lemma AreTheSame_Theorem<T>(pat: seq<T>, a: seq<T>)
ensures IsRelaxedPrefix(pat, a) == IRP_Alt(pat, a)
{
// Prove <==
if IRP_Alt(pat, a) {
if pat <= a {
Same0(pat, a);
} else if exists k :: 0 <= k < |pat| && pat[..k] + pat[k+1..] <= a {
var k :| 0 <= k < |pat| && pat[..k] + pat[k+1..] <= a;
Same1(pat, a, k);
}
assert IsRelaxedPrefix(pat, a);
}
// Prove ==>
if IsRelaxedPrefix(pat, a) {
Same2(pat, a);
assert IRP_Alt(pat, a);
}
}
lemma Same0<T>(pat: seq<T>, a: seq<T>)
requires pat <= a
ensures IsRelaxedPrefixAux(pat, a, 1)
{
}
lemma Same1<T>(pat: seq<T>, a: seq<T>, k: nat)
requires 0 <= k < |pat| && pat[..k] + pat[k+1..] <= a
ensures IsRelaxedPrefixAux(pat, a, 1)
{
// "k" gives one splitting point, but we want to last splitting point
var d := k;
while d+1 < |pat| && pat[d] == pat[d+1]
invariant 0 <= d < |pat| && pat[..d] + pat[d+1..] <= a
{
d := d + 1;
}
Same1_Aux(pat, a, d);
}
lemma Same1_Aux<T>(pat: seq<T>, a: seq<T>, k: nat)
requires 0 <= k < |pat| && pat[..k] + pat[k+1..] <= a && (k+1 == |pat| || pat[k] != pat[k+1])
ensures IsRelaxedPrefixAux(pat, a, 1)
{
if k+1 == |pat| {
assert pat[..k] + pat[k+1..] == pat[..k] <= a;
if k == 0 {
} else {
assert IsRelaxedPrefixAux(pat, a, 1) == IsRelaxedPrefixAux(pat[1..], a[1..], 1);
Same1_Aux(pat[1..], a[1..], k-1);
}
} else if k == 0 {
assert pat[..0] + pat[1..] == pat[1..];
assert pat[1] == a[0];
assert pat[0] != pat[1];
assert IsRelaxedPrefixAux(pat, a, 1) == IsRelaxedPrefixAux(pat[1..], a, 0);
Prefix(pat[1..], a);
} else {
calc ==> {
true;
pat[..k] + pat[k+1..] <= a;
(pat[..k] + pat[k+1..])[1..] <= a[1..];
pat[..k][1..] + pat[k+1..] <= a[1..];
{ assert pat[..k][1..] == pat[1..][..k-1]; }
pat[1..][..k-1] + pat[k+1..] <= a[1..];
{ assert pat[k+1..] == pat[1..][k..]; }
pat[1..][..k-1] + pat[1..][k..] <= a[1..];
}
Same1_Aux(pat[1..], a[1..], k-1);
}
}
lemma Prefix<T>(pat: seq<T>, a: seq<T>)
requires pat <= a
ensures IsRelaxedPrefixAux(pat, a, 0)
{
}
lemma Same2<T>(pat: seq<T>, a: seq<T>)
requires IsRelaxedPrefixAux(pat, a, 1)
ensures IRP_Alt(pat, a)
{
if pat == [] {
} else if a != [] && pat[0] == a[0] {
if pat[1..] <= a[1..] {
} else {
var k :| 0 <= k < |pat[1..]| && pat[1..][..k] + pat[1..][k+1..] <= a[1..];
assert 0 <= k+1 < |pat| && pat[..k+1] + pat[k+2..] <= a;
}
} else {
Same2_Prefix(pat[1..], a);
assert pat[1..] <= a;
assert 0 <= 0 < |pat| && pat[..0] + pat[0+1..] <= a;
}
}
lemma Same2_Prefix<T>(pat: seq<T>, a: seq<T>)
requires IsRelaxedPrefixAux(pat, a, 0)
ensures pat <= a
{
}
|
