1 files changed, 42 insertions, 0 deletions
diff --git a/formal/insertion.go b/formal/insertion.go
new file mode 100644
index 0000000..cf053a7
--- /dev/null
+++ b/formal/insertion.go
@@ -0,0 +1,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
+	}
+}