alt Hacker NewsYou 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?
Replies
edflsafoiewq • today at 1:58 AM
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.
➕ show 2 replies
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.