CREATE

• input: C (a collection)
• output: C'
• preconditions: C is undefined
• postconditions: C' is the empty collection. Storage is allocated as needed.

DESTROY

• input: C (a collection)
• output: C'
• preconditions: C is defined.
• postconditions: C' is undefined. All dynamically allocated memory associated with C is returned to the global pool.

SIZE

• input: C (a collection)
• output: S, a non-negative integer.
• preconditions: C is defined.
• postconditions: S = the number of elements in C.

IS_EMPTY

• input: C (a collection)
• preconditions: C is defined.
• postconditions: true if C is empty, false otherwise.