 Solution

Let $a_0$ be a saved mathematical copy of the original array. A precise postcondition for sorting isThe precondition is that a is a non-null array of length $N\ge 0$. Its length and every unrelated object remain unchanged. The second clause preserves the array multiset, including all multiplicities; ordering alone would also permit overwriting the entire array with zeros. The saved $a_0$ is a specification device and need not be allocated by the implementation.