class interface DS_BILINKABLE[G] creation make (v: G) -- Insert v in cell. ensure inserted: item = v feature(s) from DS_CELL -- Access item: G -- Content of cell feature(s) from DS_CELL -- Element change put (v: G) -- Insert v in cell. ensure inserted: item = v feature(s) from DS_CELL -- Element change make (v: G) -- Insert v in cell. ensure inserted: item = v feature(s) from DS_LINKABLE -- Access right: like Current -- Right neighbor feature(s) from DS_LINKABLE -- Element change put_right (other: like Current) -- Put other to right of cell. -- Make sure that link is bidirectional. require other_not_void: other /= Void ensure bilinked: other.left = Current; linked: right = other forget_right -- Remove right neighbor. ensure forgotten: right = Void feature(s) from DS_BILINKABLE -- Access left: like Current -- Left neighbor feature(s) from DS_BILINKABLE -- Element change put_left (other: like Current) -- Put other to left of cell. -- Make sure that link is bidirectional. require other_not_void: other /= Void ensure linked: left = other; bilinked: other.right = Current forget_left -- Remove left neighbor. ensure forgotten: left = Void end of DS_BILINKABLE[G]