|
To implement TWO_WAY_LINKED_LIST. |
| item: E_ |
| previous: TWO_WAY_LINKED_LIST_NODE [E_] |
| next: TWO_WAY_LINKED_LIST_NODE [E_] |
| set_item (i: E_) |
|
ensure
|
| set_next (n: TWO_WAY_LINKED_LIST_NODE [E_]) |
|
ensure
|
| set_all_with (v: E_) |
| set_previous (p: TWO_WAY_LINKED_LIST_NODE [E_]) |
|
ensure
|