Specifications Of Collection And List

A collection is a set of elements, all of which are the same type. A list is a special kind of collection, with two extra properties:

in a list there is a linear order (called `followed by', or `next') defined on the elements: every element (except for one, called the last element ) is followed by one other element, and no two elements are followed by the same element. There is exactly one element in a list (the first element) that does not follow after any element.
It is possible to access individual elements of a list. This access is provided by having a `window' on the list; when we define the abstract type List we will also have to define `window'.

Operations on a Collection

Notation: when we have an input X, an output of X' (X-prime) indicates that the value of X is changed by the procedure.

create

Input: C (a collection)
Output: C' (means C is changed - see above)
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.

This is the inverse of create

is_empty

Input: C (a collection)
Preconditions: C is defined.
Postconditions: true if C is empty, false otherwise

size

Input: C (a collection)
Output: S (non-negative integer)
Preconditions: C is defined
Postconditions: S = the number of elements in C

insert

Input: C (a collection), V (a value)
Output: C'
Preconditions: V is of a type suitable for collection elements
Postconditions: C' = C with value V added. Storage is allocated as needed. If V already occurs in C, C' contains an additional copy of V.

delete

Input: C (a collection), V (a value)
Output: C'
Preconditions: V is of a type suitable for collection elements
Postconditions: C' = C with value V removed. If V does not occur in C, the operation does nothing. If there are several copies of V in C, just one is deleted. If possible, the storage associated with the deleted occurrence of V is returned to the global pool.

join

Input: C1 and C2 (collections)
Output: C1' and C2'
Preconditions: C1 and C2 are both defined, and are different collections.
Postconditions: C1' is the union of the two collections (i.e. it contains all the elements in C1 and C2). C2' is undefined.

map

Input: C (a collection), P (a procedure), D extra data parameter for P.
Output: determined by P
Preconditions: C is defined. P takes two parameters: the first is of type pointer to `collection element' and the second is D.
Postconditions: P has been called with every element in C

Operations on a List

All the above operations apply to lists: a list may be used wherever a collection is required. Because lists have extra structure - the order on the elements - there are additional postconditions on some operations. None of the operations change the order of elements, except as stated explicitly.

insert

Postconditions: C' = C with value V added. Storage is allocated as needed. If V already occurs in C, C' contains an additional copy of V. If C is a list: V is the first element in C'.

delete

Postconditions: C' = C with value V removed. If V does not occur in C, the operation does nothing. If there are several copies of V in C, just one is deleted. If possible, the storage associated with the deleted occurrence of V is returned to the global pool. If C is a list: the first occurrence of V in C is the one that is deleted.

join

Postconditions: C1' is the union of the two collections (i.e. it contains all the elements in C1 and C2). C2' is undefined. If C1 and C2 are lists: in C1' the elements of C1 and C2 are in their original order, and the elements of C1 are before the elements of C2.

map

Postconditions: P has been called with every element in C. If C is a list: if E1 occurs before E2 in C, then the call P(E1) is made before the call P(E2).

Additional Operations For Lists And Windows

create_window

Input: L (a list), W (a window)
Output: W'
Preconditions: L is not empty. W is undefined.
Postconditions: W' is on the first element in L. Storage is allocated as needed.

destroy_window

Input: W (a window)
Output: W'.
Preconditions: none.
Postconditions: W' is undefined. As much space is reclaimed as is possible.

is_last

Input: W (a window)
Output: boolean
Preconditions: W is defined
Postconditions: true if W is on the last element in a list, false otherwise

get_value

Input: W (a window)
Output: V (a value of a list element)
Preconditions: W is defined
Postconditions: V is the value of the element W is on

move_forward

Input: W (a window)
Output: W'
Preconditions: W is not on the last element of a list
Postconditions: W' is on the element that follows the element W was on

split

Input: L1, L2 (lists), W (a window)
Output: L1' and L2'
Preconditions: W is a window into L1, L2 is undefined
Postconditions: L2' = the elements of L1 following the one W is on, their order unchanged. If W is on the last element, L2' is empty. L1' = the elements of L1 up to and including the one W is on, their order unchanged.