4 ms·
It was touched upon in the post: 'Tip: Don’t prove what you don’t need to prove' (and surrounding text). With a link on another proof for another sorting algori
by touisteur 4y ago
It was touched upon in the post: 'Tip: Don’t prove what you don’t need to prove' (and surrounding text). With a link on another proof for another sorting algorithm.
- yannickmoy 4y agoand there are actually multiple ways to prove that the result is a permutation of the entry, either by computing a model multiset (a.k.a. bag) of the value on entry and exit and showing they are equal, or by exhibiting the permutation to apply to the entry value to get the exit value (typically by building this permutation as the algorithm swaps value, in ghost code), etc. but none of this makes a good read for people not already familiar with program proof tools.