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.