[zozbot234]

To be clear, the proper postcondition for a sort function is "the output array is a permutation of the input array and it is sorted".