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