3 ms·
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` bein
by samus 2mo ago
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.
- inigyou 2mo agoyou 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
- samus 2mo agoMy 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.