To implement TWO_WAY_LINKED_LIST. |
make (i: E_, p: TWO_WAY_LINKED_LIST_NODE [E_], n: TWO_WAY_LINKED_LIST_NODE [E_]) |
ensure
|
item: E_ |
previous: TWO_WAY_LINKED_LIST_NODE [E_] |
next: TWO_WAY_LINKED_LIST_NODE [E_] |
make (i: E_, p: TWO_WAY_LINKED_LIST_NODE [E_], n: TWO_WAY_LINKED_LIST_NODE [E_]) |
ensure
|
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
|