Specification of Table

key

• Input: C, a component
• Output: K, a key
• Preconditions: none
• Postconditions: K is C's key

data

• Input: C, a component
• Output: D, data
• Preconditions: none
• Postconditions: D is C's data

create

• Input: T, a table
• Output: T' (i.e. T initialized)
• Preconditions: T is undefined
• Postconditions: T' is empty

destroy

• Input: T, a table
• Output: T'
• Preconditions: T is defined
• Postconditions: T' is undefined

is_empty

• Input: T, a table
• Output: a boolean
• Preconditions: none
• Postconditions: the boolean is true if T is empty, false otherwise.

is_full

• Input: T, a table
• Output: a boolean
• Preconditions: none
• Postconditions: the boolean is true if T is full, false otherwise.

insert

• Inputs: C, a component, T, a table
• Output: T'
• Preconditions: T contains no component with the same key as C
• Postconditions: T' is T with C added.

Alternatively, we could drop the precondition and modify the postconditions as follows: if T contains a component C2 with the same key as C, then T' is like T but with C2 removed and C added. In other words, C replaces C2.

delete

• Input: K, a key, T, a table
• Output: T'
• Preconditions: none
• Postconditions: T' is T with all components with key K removed.

retrieve

• Inputs: K, a key, T, a table
• Outputs: C, a component, F, a boolean
• Preconditions: none
• Postconditions: if T contains a component with key K, then C is this component and F is true, otherwise F is false (and there is no condition on C).