Comment by samus | Hacker News Reader

Comment by samus | Hacker News Reader

Parent Full thread

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.

you have the common problems with non-uniqueness and with extra elements. Your spec is met by:

    SORT(1,2,3,4,5,5,6) = 1,2,3,4,5,6

    SORT(1,2,3,4,5,5,6) = 1,2,3,4,5,6,7

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.

Reply on news.ycombinator.com