Comment by inigyou
3 hours ago
You know, the last time someone brought up formal verification of sorting I said what the trivial spec was, and then someone else pointed out why it's actually completely wrong.
So for pedagogical purposes, can you tell us what you think the trivial spec is?
Ok, I’ll bite, why is this wrong?
For a list of items I and an operator LEQ which returns bool for any pair of items in I, SORT() returns a list S such that:
1. Every item in I is present exactly once in S
2. For each consecutive pair of items (S_i, S_j) in S, LEQ(S_i, S_j) is true.
SORT(1,2,3,4,5,5,6) = 1,2,3,4,5,6
I'm sorry, do all 5's look the same to you!! /s
aka, one item in I is missing in your output.
12 replies →
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.
See how easy it is once you have right terms ;)