Let denote the entry state. A conventional meaning for the Boolean returned by Initially . In particular, re-adding an existing element returns false and does not increase the size. All operations have the stated empty precondition at the abstract level. The comment that
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)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. Articles by others on the same topic
There are currently no matching articles.