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
	}
}