= Solution
Let $S_0$ denote the entry state. A conventional meaning for the Boolean returned by `add` is whether the call changes the <set>:
``
// add(elem):
// S' = S0 union {elem}
// result == !S0.contains(elem)
// contains(elem):
// S' = S0
// result == S0.contains(elem)
// size:
// S' = S0
// result == cardinality(S0)
``
Initially $S=\varnothing$. In particular, re-adding an existing element returns false and does not increase the size. \b[All operations have the stated empty <precondition>] at the abstract level. The comment that `add` adds an element does not itself completely specify its Boolean result; the explicit changed/not-changed convention above completes that contract. As with any `Int`-valued size operation, exact cardinalities are understood to be representable by that result type.
Back to article page
