blob: cf053a7fc0d78ea2f6fe692b84969cdf38c35c2f (
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
|
package formal
// Insertion sorts a in ascending order, in place. This is a monomorphized
// (non-generic, plain []int, inlined swap) copy of sort.Insertion, annotated so
// the Gobra verifier can prove -- with the Viper/Z3 backend -- BOTH:
//
// 1. memory safety: every index access is in bounds (the permission
// invariants "forall k :: 0<=k<len(a) ==> acc(&a[k])" carry write access
// to every element through both loops), and
// 2. functional correctness (ordering): on return, a is sorted ascending
// (the postcondition "forall p<q :: a[p] <= a[q]").
//
// The permutation half of correctness (that the output is a rearrangement of
// the input) is left to the property tests + the paper proof in
// docs/verification.md; proving it here would require ghost multiset state.
//
//@ 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 Insertion(a []int) {
i := 0
//@ invariant 0 <= i && i <= len(a)
//@ invariant forall k int :: 0 <= k && k < len(a) ==> acc(&a[k])
// The prefix a[0..i) is already fully sorted.
//@ invariant forall p, q int :: 0 <= p && p < q && q < i ==> a[p] <= a[q]
for i < len(a) {
j := i
//@ invariant 0 <= j && j <= i && i < len(a)
//@ invariant forall k int :: 0 <= k && k < len(a) ==> acc(&a[k])
// a[0..i] is sorted once position j is ignored as either endpoint...
//@ invariant forall p, q int :: 0 <= p && p < q && q <= i && p != j && q != j ==> a[p] <= a[q]
// ...and the in-flight element a[j] is <= everything to its right.
//@ invariant forall q int :: j < q && q <= i ==> a[j] <= a[q]
for j > 0 && a[j] < a[j-1] {
tmp := a[j]
a[j] = a[j-1]
a[j-1] = tmp
j = j - 1
}
i = i + 1
}
}
|
