Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Imperative programming / 3 / a

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.