deferred class interface DS_NESTED_LIST[G] feature(s) from DS_NESTED_LIST -- Access local_items: DS_LINEAR[G] -- Items held locally ensure local_items_not_void: Result /= Void remote_items: DS_LINEAR[DS_NESTED_LIST[G]] -- Items held by other lists ensure remote_items_not_void: Result /= Void; no_void_remote: not Result.has(Void) end of deferred DS_NESTED_LIST[G]