3 ms·
Why not check in $n$ on a sorted if the postcondition holds or raise an exception otherwise. You can even generate a nearly sorted list and run a verified bubbl
by riedel 6y ago
Why not check in $n$ on a sorted if the postcondition holds or raise an exception otherwise. You can even generate a nearly sorted list and run a verified bubblesort. Don't see big problems if ML is used carefully.
- fdupress 6y agoChecking that the output is sorted is the easy part. Checking that the output is a (optionally stable) permutation of the input is the hard part. You can't do that dynamically if you have, for example, overwritten your input by sorting in place. And making a copy of your input is only going to be affordable in very specific and small instances on which you might as well just run a well-understood algorithm.
- ogogmad 6y agoIt looks like their algorithm can only modify the input list by swapping elements. This is guaranteed to result in a permutation.