Specification Examples
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.
order makes sense for the elements.