Definition
An instance of the data type node_list is a doubly linked list of nodes. It is implemented more efficiently than the general list type list<node> (Linear Lists). However, it can only be used with the restriction that every node is contained in at most one node_list.
Creation
| node_list | L; | introduces a variable L of type node_list and initializes it with the empty list. |
|
Operations
| void | L.append(node v) | appends v to list L. |
| void | L.push(node v) | adds v at the front of L. |
| void | L.insert(node v, node w) | inserts v after w into L.
Precondition: w in L. |
| node | L.pop() | deletes the first node from L and returns it.
Precondition: L is not empty. |
| void | L.del(node v) | deletes v from L.
Precondition: v in L. |
| bool | L.member(node v) | returns true if v in L and false otherwise. |
| bool | L(node v) | returns true if v in L and false otherwise. |
| node | L.first() | returns the first node in L (nil if L is empty). |
| node | L.last() | returns the last node in L (nil if L is empty). |
| node | L.succ(node v) | returns the successor of v in L.
Precondition: v in L. |
| node | L.pred(node v) | returns the predecessor of v in L.
Precondition: v in L. |
| node | L.cyclic_succ(node v) | returns the cyclic successor of v in L.
Precondition: v in L. |
| node | L.cyclic_pred(node v) | returns the cyclic predecessor of v in L.
Precondition: v in L. |
| bool | L.empty() | returns true if L is empty and false otherwise. |
forall(x,L)
``the elements of L are successively assigned to x'' 