Trivial one: `forall i, j. 0 <= i < j < |sorted| -> sorted[i] <= sorted[j]`, which can be satisfied by copying a single element from `input` or by `sorted` being empty.
It can be fixed (feedback welcome) by adding: `forall i, j. 0 <= i < |sorted| -> |indexof_id(sorted, input[i])| = 1`, with `indexof_id` using equality by identity, which is crucial in practice.
Note that the amended definition implies quadratic runtime, which is the crucial difference between a specification and an efficient implementation.
and a bounds checking bug unique to your formal spec because you only check inputs up to the length of the output
// first 0 elements of input must occur in output
SORT(1,2,3,4,5,5,6) = empty list
// first 6 elements of input must occur in output
SORT(1,2,3,4,5,5,6) = 1,2,3,4,5,7
My second condition would reject the additional element, as it would not be found in the input. have to be duplicated to However, I was lazy about the `|input| = |output|` constraints. With those constraints it would not be possible to omit elements from the input in the output.
It can be fixed (feedback welcome) by adding: `forall i, j. 0 <= i < |sorted| -> |indexof_id(sorted, input[i])| = 1`, with `indexof_id` using equality by identity, which is crucial in practice.
Note that the amended definition implies quadratic runtime, which is the crucial difference between a specification and an efficient implementation.