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
|
(** Insertion sort.
Surprinsingly, the verification of insertion sort is more difficult
than the proof of other, more efficient, sorting algorithms.
One reason is that insertion sort proceeds by shifting elements,
which means that, within the inner loop, the array is *not* a permutation
of the initial array. Below we make use of the functional array update
a[j <- v] to state that, if ever we put back `v` at index `j`, we get
an array that is a permutation of the original array.
*)
module InsertionSort
use int.Int
use array.Array
use array.IntArraySorted
use array.ArrayPermut
use array.ArrayEq
let insertion_sort (a: array int) : unit
ensures { sorted a }
ensures { permut_all (old a) a }
= for i = 1 to length a - 1 do
(* a[0..i[ is sorted; now insert a[i] *)
invariant { sorted_sub a 0 i /\ permut_all (old a) a }
let v = a[i] in
let ref j = i in
while j > 0 && a[j - 1] > v do
invariant { 0 <= j <= i }
invariant { permut_all (old a) a[j <- v] }
invariant { forall k1 k2.
0 <= k1 <= k2 <= i -> k1 <> j -> k2 <> j -> a[k1] <= a[k2] }
invariant { forall k. j+1 <= k <= i -> v < a[k] }
variant { j }
label L in
a[j] <- a[j - 1];
assert { exchange (a at L)[j <- v] a[j-1 <- v] (j - 1) j };
j <- j - 1
done;
assert { forall k. 0 <= k < j -> a[k] <= v };
a[j] <- v
done
let test1 () =
let a = make 3 0 in
a[0] <- 7; a[1] <- 3; a[2] <- 1;
insertion_sort a;
a
let test2 () ensures { result.length = 8 } =
let a = make 8 0 in
a[0] <- 53; a[1] <- 91; a[2] <- 17; a[3] <- -5;
a[4] <- 413; a[5] <- 42; a[6] <- 69; a[7] <- 6;
insertion_sort a;
a
exception BenchFailure
let bench () raises { BenchFailure -> true } =
let a = test2 () in
if a[0] <> -5 then raise BenchFailure;
if a[1] <> 6 then raise BenchFailure;
if a[2] <> 17 then raise BenchFailure;
if a[3] <> 42 then raise BenchFailure;
if a[4] <> 53 then raise BenchFailure;
if a[5] <> 69 then raise BenchFailure;
if a[6] <> 91 then raise BenchFailure;
if a[7] <> 413 then raise BenchFailure;
a
end
module InsertionSortGen
use int.Int
use array.Array
use array.ArrayPermut
use array.ArrayEq
type elt
val predicate le elt elt
clone map.MapSorted as M with type elt = elt, predicate le = le
axiom le_refl: forall x:elt. le x x
axiom le_asym: forall x y:elt. not (le x y) -> le y x
axiom le_trans: forall x y z:elt. le x y /\ le y z -> le x z
predicate sorted_sub (a : array elt) (l u : int) =
M.sorted_sub a.elts l u
predicate sorted (a : array elt) =
M.sorted_sub a.elts 0 a.length
let insertion_sort (a: array elt) : unit
ensures { sorted a }
ensures { permut_all (old a) a }
= for i = 1 to length a - 1 do
(* a[0..i[ is sorted; now insert a[i] *)
invariant { sorted_sub a 0 i }
invariant { permut_all (old a) a }
let v = a[i] in
let ref j = i in
while j > 0 && not (le a[j - 1] v) do
invariant { 0 <= j <= i }
invariant { permut_all (old a) a[j <- v] }
invariant { forall k1 k2.
0 <= k1 <= k2 <= i -> k1 <> j -> k2 <> j -> le a[k1] a[k2] }
invariant { forall k. j+1 <= k <= i -> le v a[k] }
variant { j }
label L in
a[j] <- a[j - 1];
assert { exchange (a at L)[j <- v] a[j-1 <- v] (j - 1) j };
j <- j - 1
done;
assert { forall k. 0 <= k < j -> le a[k] v };
a[j] <- v
done
end
(** Using swaps (instead of shifting) is less efficient but at least
we can expect the loop invariant for the inner loop to be
simpler. And indeed it is.
The invariant below was suggested by Xavier Leroy (Collège de France).
Without surprise, the proof of the permutation property is also simpler.
*)
module InsertionSortSwaps
use int.Int
use array.Array
use array.ArraySwap
use array.ArrayPermut
let insertion_sort (a: array int) : unit
ensures { forall p q. 0 <= p <= q < length a -> a[p] <= a[q] }
ensures { permut_all (old a) a }
= for i = 1 to length a - 1 do
invariant { forall p q. 0 <= p <= q < i -> a[p] <= a[q] }
invariant { permut_all (old a) a }
let ref j = i in
while j > 0 && a[j - 1] > a[j] do
invariant { 0 <= j <= i }
invariant { permut_all (old a) a }
invariant { forall p q. 0 <= p <= q <= i -> q <> j -> a[p] <= a[q] }
variant { j }
swap a (j - 1) j;
j <- j - 1
done
done
end
|
