class interface DIRECTORY -- -- Tools for file-system directory handling. -- -- Clean hight-level facade for class BASIC_DIRECTORY. -- creation connect_to (new_path: STRING) require not new_path.empty feature(s) from DIRECTORY is_connected: BOOLEAN feature(s) from DIRECTORY -- Creation / Modification : connect_to (new_path: STRING) require not new_path.empty feature(s) from DIRECTORY -- Access : lower: INTEGER -- Index of the first item. upper: INTEGER -- Index of the last item. count: INTEGER -- Number of items (files or directories) in Current. ensure Result >= 0 valid_index (index: INTEGER): BOOLEAN ensure Result = index.in_range(1,count) path: STRING require is_connected name (index: INTEGER): STRING -- Return the name of entry (file or subdirectory) at index. require is_connected; valid_index(index) ensure has(Result) has (entry_name: STRING): BOOLEAN -- Does Current contain the entry_name (file or subdirectory) ? require is_connected; not entry_name.empty end of DIRECTORY