Comment by edflsafoiewq
1 day ago
1. The output is a permutation of the input.
2. If the comparison implements a strict total order, the output is sorted according to it.
1 day ago
1. The output is a permutation of the input.
2. If the comparison implements a strict total order, the output is sorted according to it.
You are correct.
However, that specification is not trivial. Almost nobody correctly articulates property 1 when first encountering the problem if they do not already know the answer or are already aware it is a trick question (and even then most software developers still fail).
Furthermore, that also sidesteps the problem of formally specifying what a permutation is. Unless you have a grab bag of already proven powerful theorems, the author is most likely also going to make a error doing that as well even if we start at a proof abstraction level comparable to normal programming.
Reality is that trivial problems admit trivially wrong specifications exceedingly easily. There is little reason to assume that much more complicated problems that are hard to even articulate will magically support obviously correct specifications that are simpler and more understandable than the code.
Note this doesn't make it useless, just not watertight. Proving that the output of a sort algorithm is a sorted list is genuinely useful and catches a lot of potential bugs. If your sort algorithm is "return []" you'll certainly notice that while writing the proof and fix it. It'll also be caught easily by any unit test.
It wouldn't catch all bugs - merge sort recursing on the same half of the list both times would return one item N times, which is sorted, and is a plausible enough mistake to make.
I think this works, but I could be proven wrong yet again.
You might also want to prove that the comparison implements a strict total order, but that would be part of the comparison's spec, not the sorting function's. There is another possibility for a mistake there: if you don't use exactly the same test, you might prove that your < implements a strict total order by its definition, while also proving it doesn't according to the sort function spec and thus allowing the sort to return anything.
See how easy it is once you have right terms ;)