= Solution
Let $a_0$ be a saved mathematical copy of the original <array>. A precise <postcondition> for <sorting> is
$$
\boxed{\begin{aligned}
&\forall i,j\in[0,N):\ i<j\Longrightarrow a(i)\leq a(j),\\
&\forall v\in\mathbb Z:\ \#\{i:a(i)=v\}=\#\{i:a_0(i)=v\}.
\end{aligned}}
$$
The <precondition> is that `a` is a non-null <array> of length $N\geq0$. 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.
Back to article page
