[Jtsummers]

> for each pair of two elements, the one that comes first is less than or equal to the one that comes second.

That's the property that the result is sorted, but not that you've performed the desired task of sorting a particular list. You also need a post-condition saying that each item in the original is in the destination and with the same number of occurrences.

If you just require that the result be sorted, then this is a valid sort:

  def sorted(ls):
    return []

If you require that it be sorted and contain the same items (but don't check the count), then this is technically sufficient (I've abstracted the actual sort operation out):

  def sorted(ls):
    ls = list(set(ls)) # removes duplicates
    # perform sort
    return result

If you get to the right post-condition, it has to have the same items and the same count and be sorted, then it will satisfy this test:

  def sorted_postcondition(original, result):
    return all(x <= y for x, y in pairwise(result)) and Counter(original) == Counter(result) # Counter is being used as a multiset

[touisteur]

Yes it gets hard really fast. We had a fun (if tongue-in-cheek) exploration of this (proving a sort implementation) with Yannick Moy of SPARK fame some time ago https://www.adacore.com/blog/i-cant-believe-that-i-can-prove...

I only regret not writing the obvious-but-buggy code that "forgot" or added some values and still passed proof...

[pocksuppet]

Aaaaaand now it's a good demonstration of why specifications are not as easy as they seem.

[Jtsummers]

It mostly just takes practice. A good way to get into it is with property-based testing. It's less formal, but you end up expressing many of the same things (you're at least expressing the post-conditions, if not the rest of the things needed for a proof). With practice, you'll start to understand your systems better, and things like what I wrote up will come to you more easily when analyzing and designing them.

To move towards formal proofs of code, I like Leino's Program Proofs (uses Dafny), one of the more approachable tutorials on the subject.

[teiferer]

> It mostly just takes practice

If practice is enough to get a formal system to be correct then why are we doing all this in the first place? Just write correct software! Oh, you can make mistakes? Exaclty! Just like when writing the spec.

[Jtsummers]

> If practice is enough

If that is what you got from my comment, then you did not read my comment.