Hacker News new | past | comments | ask | show | jobs | submit login

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.



Checking 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.


It looks like their algorithm can only modify the input list by swapping elements. This is guaranteed to result in a permutation.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: