3 ms·

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

• pastel8739 3mo ago
  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.
  • inigyou 3mo ago
    SORT(1,2,3,4,5,5,6) = 1,2,3,4,5,6
    • defrost 3mo ago
      I'm sorry, do all 5's look the same to you!! /s aka, one item in I is missing in your output.
      • inigyou 3mo ago
        No, if it had one more 5 it would violate your specification that every time must occur exactly once. Also, SORT(1,2,3,4) = 1,2,3,4,7
        • defrost 3mo ago
          Not my specification (drive by third party) but I do take the view that ( 1, 2, 3, 4, 5, 5, 6 ) is a list of seven values (perhaps the number of dollars in the pockets of seven distinct unique people) and when sorted the output should also have seven items that correspond to the seven input items. > Also ... Yeah, that needs tightening up by pastel8739
          • Jtsummers 3mo ago
            You need a way to differentiate the two 5s, that isn't present. If you had a list like: L = [(5,foo), (2,bar), (2,baz),...] And did a: SORT(L, key=first) # or however it'd be specified Then the duplicate 2s would be fine, because they're no longer duplicates, only duplicate keys. But it would still fail if (2,baz) showed up twice in the source and destination even though we've asked for SORT, not UNIQSORT.
            • defrost 3mo ago
              In the cases of SORT ( 3, 2, 5, 5 ) ->> ( 2, 3, 5, 5 ) and SORT ( 3, 2, 5, 5 ) ->> ( 2, 3, 5, 5 ) one or both of those might be incorrect ? ( I'm teasing, perhaps )
            • defrost 3mo ago
              More seriously, > You need a way to differentiate the two 5s As there's no unique filtering or other reduction going on here, there's a permutation chain from input to output.
              • Jtsummers 3mo ago
                But that's not in the specification given above. That specification is entirely wrong to specify SORT. It requires no duplicates survive the sorting process.
          • inigyou 3mo ago
            The specification said Every item in I is present exactly once in S 5 is an item in I, and it is present exactly once in S.
            • defrost 3mo ago
              and 5 is another item in I, and it's not present in S.
              • 3mo ago
      • Jtsummers 3mo ago
        > I'm sorry, do all 5's look the same to you!! /s You have that /s tag, but this is actually the problem with pastel8739's spec as written. >> 1. Every item in I is present exactly once in S This actually does require inigyou's example to be the result of calling SORT when you cannot distinguish repeated items from each other. SORT([1,1]) => [1,1] The item 1 (which one? doesn't matter, they both do but we only need one to fail the post-condition to invalidate the result) in the source list has a count of 2 in the destination list, so this is an invalid result by the supplied spec. pastel8739's spec also doesn't exclude the possibility of inserting new values (so long as they aren't duplicates of items in the source list).
• edflsafoiewq 3mo 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.
  • esafak 3mo ago
    See how easy it is once you have right terms ;)
  • Veserv 3mo ago
    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.
    • inigyou 3mo ago
      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.
  • inigyou 3mo ago
    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.
• samus 3mo 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 3mo ago
    you 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 ago
      My 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.