blob: 1a9028d6e538d2065321071cec917d9d8ac3d3bb (
plain)
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
|
package formal
// Selection sorts a in ascending order, in place. This is a monomorphized
// (non-generic, plain []int, inlined swap, no `continue`) copy of
// sort.Selection, annotated so Gobra proves memory safety AND that the result
// is sorted ascending, for all inputs.
//
// Selection sort's proof needs a stronger outer invariant than insertion sort:
// not only is the prefix a[0..i) sorted, but every element of that prefix is
// <= every element of the unsorted suffix a[i..len). That second invariant is
// what lets the newly selected minimum extend the sorted prefix.
//
//@ requires forall k int :: 0 <= k && k < len(a) ==> acc(&a[k])
//@ ensures forall k int :: 0 <= k && k < len(a) ==> acc(&a[k])
//@ ensures forall p, q int :: 0 <= p && p < q && q < len(a) ==> a[p] <= a[q]
func Selection(a []int) {
i := 0
//@ invariant 0 <= i && i <= len(a)
//@ invariant forall k int :: 0 <= k && k < len(a) ==> acc(&a[k])
// a[0..i) is sorted...
//@ invariant forall p, q int :: 0 <= p && p < q && q < i ==> a[p] <= a[q]
// ...and every prefix element is <= every suffix element.
//@ invariant forall p, q int :: 0 <= p && p < i && i <= q && q < len(a) ==> a[p] <= a[q]
for i < len(a) {
min := i
j := i + 1
//@ invariant i < len(a) && i+1 <= j && j <= len(a)
//@ invariant i <= min && min < len(a)
//@ invariant forall k int :: 0 <= k && k < len(a) ==> acc(&a[k])
// a[min] is the smallest of the scanned suffix a[i..j).
//@ invariant forall k int :: i <= k && k < j ==> a[min] <= a[k]
// The outer invariants still hold (the inner loop reads only).
//@ invariant forall p, q int :: 0 <= p && p < q && q < i ==> a[p] <= a[q]
//@ invariant forall p, q int :: 0 <= p && p < i && i <= q && q < len(a) ==> a[p] <= a[q]
for j < len(a) {
if a[j] < a[min] {
min = j
}
j = j + 1
}
if min != i {
tmp := a[i]
a[i] = a[min]
a[min] = tmp
}
i = i + 1
}
}
|
