lAn array-sorting program:
lInput assertion: a == a0
lOutput assertion:
lThe elements of a are those of a0 as a ÒbagÓ (or Òmulti-setÓ) i.e. the same number of each
element.
lThe elements of a are in increasing order
lImplicit here is that the notion that
order makes sense for the
elements.