(no title)
ookdatnog | 2 months ago
Take sorting a list for example. The spec is quite short.
- for all xs: xs is a permutation of sort(xs)
- for all xs: sorted(sort(xs))
Where we can define "xs is a permutation of ys" as "for each x in xs: occurrences(x, xs) = occurrences(x, ys)"
And "sorted(l)" as "forall xs, x, y, ys: (l = xs ++ [x, y] ++ ys) => x < y".
A straightforward bubble or insertion sort would perhaps be considered as simple or simpler than this spec. But the sorting algorithms in, say, standard libraries, tend to be significantly more complex than this spec.
No comments yet.