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
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
abstract module TotalOrder {
type T // the type to be compared
predicate method Leq(a: T, b: T) // Leq(a,b) iff a <= b
// Three properties of total orders. Here, they are given as unproved
// lemmas, that is, as axioms.
lemma Antisymmetry(a: T, b: T)
requires Leq(a, b) && Leq(b, a);
ensures a == b;
lemma Transitivity(a: T, b: T, c: T)
requires Leq(a, b) && Leq(b, c);
ensures Leq(a, c);
lemma Totality(a: T, b: T)
ensures Leq(a, b) || Leq(b, a);
}
abstract module Sort {
import O as TotalOrder // let O denote some module that has the members of TotalOrder
predicate Sorted(a: array<O.T>, low: int, high: int)
requires a != null && 0 <= low <= high <= a.Length;
reads a;
// The body of the predicate is hidden outside the module, but the postcondition is
// "exported" (that is, visible, known) outside the module. Here, we choose the
// export the following property:
ensures Sorted(a, low, high) ==> forall i, j :: low <= i < j < high ==> O.Leq(a[i], a[j]);
{
forall i, j :: low <= i < j < high ==> O.Leq(a[i], a[j])
}
// In the insertion sort routine below, it's more convenient to keep track of only that
// neighboring elements of the array are sorted...
predicate NeighborSorted(a: array<O.T>, low: int, high: int)
requires a != null && 0 <= low <= high <= a.Length;
reads a;
{
forall i :: low < i < high ==> O.Leq(a[i-1], a[i])
}
// ...but we show that property to imply all pairs to be sorted. The proof of this
// lemma uses the transitivity property.
lemma NeighborSorted_implies_Sorted(a: array<O.T>, low: int, high: int)
requires a != null && 0 <= low <= high <= a.Length;
requires NeighborSorted(a, low, high);
ensures Sorted(a, low, high);
decreases high - low;
{
if low != high {
NeighborSorted_implies_Sorted(a, low+1, high);
forall j | low+1 < j < high
{
O.Transitivity(a[low], a[low+1], a[j]);
}
}
}
// Standard insertion sort method
method InsertionSort(a: array<O.T>)
requires a != null;
modifies a;
ensures Sorted(a, 0, a.Length);
ensures multiset(a[..]) == old(multiset(a[..]));
{
if a.Length == 0 { return; }
var i := 1;
while i < a.Length
invariant 0 < i <= a.Length;
invariant NeighborSorted(a, 0, i);
invariant multiset(a[..]) == old(multiset(a[..]));
{
var j := i;
while 0 < j && !O.Leq(a[j-1], a[j])
invariant 0 <= j <= i;
invariant NeighborSorted(a, 0, j);
invariant NeighborSorted(a, j, i+1);
invariant 0 < j < i ==> O.Leq(a[j-1], a[j+1]);
invariant multiset(a[..]) == old(multiset(a[..]));
{
// The proof of correctness uses the totality property here.
// It implies that if two elements are not previously in
// sorted order, they will be after swapping them.
O.Totality(a[j-1], a[j]);
a[j], a[j-1] := a[j-1], a[j];
j := j - 1;
}
i := i + 1;
}
NeighborSorted_implies_Sorted(a, 0, a.Length);
}
}
// Natural ordering of the integers
module IntOrder refines TotalOrder {
// Instantiate type T with a datatype wrapper around an integer.
// (If there were type synonyms, we could perhaps have written just "type T = int".)
datatype T = Int(i: int)
// Define the ordering on these integers
predicate method Leq ...
ensures Leq(a, b) ==> a.i <= b.i;
{
a.i <= b.i
}
// The three required properties of the order are proved here as lemmas.
// The proofs are automatic and don't require any further assistance.
lemma Antisymmetry ... { }
lemma Transitivity ... { }
lemma Totality ... { }
}
// Another example of a TotalOrder. Now we can sort pairs of integers.
// Lexiographic ordering of pairs of integers
module IntLexOrder refines TotalOrder {
datatype T = Int(i: int, j: int)
predicate method Leq ... {
if a.i < b.i then true
else if a.i == b.i then a.j <= b.j
else false
}
lemma Antisymmetry ... { }
lemma Transitivity ... { }
lemma Totality ... { }
}
// A test harness.
module Client {
module IntSort refines Sort { // this creates a new sorting module, like Sort by fully revealing O to be IntOrder
import O = IntOrder
}
import I = IntOrder
method TheMain() {
var a := new I.T[4];
a[0] := I.T.Int(6); // alternatively, we could have written the RHS as: IntSort.O.T.Int(6)
a[1] := I.T.Int(1);
a[2] := I.T.Int(0);
a[3] := I.T.Int(4);
// These are now the elements of the array:
assert a[..] == [I.T.Int(6), I.T.Int(1), I.T.Int(0), I.T.Int(4)];
// Call the sorting routine to sort the array
IntSort.InsertionSort(a);
// Check the answer
assert IntSort.O.Leq(a[0], a[1]); // lemma
assert IntSort.O.Leq(a[1], a[2]); // lemma
assert IntSort.O.Leq(a[2], a[3]); // lemma
assert a[..] == [I.T.Int(0), I.T.Int(1), I.T.Int(4), I.T.Int(6)];
// why not print out the result!
print a[..], "\n";
}
}
// ----- Now for the actual 'int' type -----
module intOrder refines TotalOrder {
// Instantiate type T with a datatype wrapper around an integer.
type T = int
// Define the ordering on these integers
predicate method Leq ...
ensures Leq(a, b) ==> a <= b;
{
a <= b
}
// The three required properties of the order are proved here as lemmas.
// The proofs are automatic and don't require any further assistance.
lemma Antisymmetry ... { }
lemma Transitivity ... { }
lemma Totality ... { }
}
module AnotherClient {
module intSort refines Sort {
import O = intOrder
}
import I = intOrder
method TheMain() {
var a := new int[4]; // alternatively, could have written 'new I.T[4]'
a[0] := 6;
a[1] := 1;
a[2] := 0;
a[3] := 4;
// These are now the elements of the array:
assert a[..] == [6, 1, 0, 4];
// Call the sorting routine to sort the array
intSort.InsertionSort(a);
// Check the answer
assert intSort.O.Leq(a[0], a[1]); // lemma
assert intSort.O.Leq(a[1], a[2]); // lemma
assert intSort.O.Leq(a[2], a[3]); // lemma
assert a[..] == [0, 1, 4, 6];
// why not print out the result!
print a[..], "\n";
}
}
method Main() {
Client.TheMain();
AnotherClient.TheMain();
}
|
