class interface F_FILE_SYSTEM creation make -- Create object. feature(s) from F_FILE_SYSTEM -- File system free_disk_space (drivename: STRING): INTEGER -- Return free disk space in KILOBYTES (1024 bytes). require valid_str: drivename /= Void ensure done: -- last_success implies last_size set feature(s) from F_FILE_SYSTEM -- Directories is_directory (pathname: STRING): BOOLEAN -- Is pathname a file directory? require valid_str: pathname /= Void create_directory (pathname: STRING) -- Create directory pathname. require valid_str: pathname /= Void; not_dir: not is_directory(pathname) ensure done: last_success implies is_directory(pathname) remove_directory (pathname: STRING) -- Remove directory pathname. require valid_str: pathname /= Void; not_dir: is_directory(pathname); -- is_empty_directory (pathname) empty: ensure done: last_success implies not is_directory(pathname) directory_content (pattern: STRING) -- Get list of files and directories in this directory. -- May include * and ? wildcards. require valid_str: pattern /= Void ensure done: last_success implies last_content /= Void -- and set. current_directory -- Get current directory. ensure done: -- last_success implies last_directory set change_current_directory (newdir: STRING) -- Change current directory. temporary_directory -- Get temporary directory. feature(s) from F_FILE_SYSTEM -- File is_file (fname: STRING): BOOLEAN -- Does the file fname exists? require valid_str: fname /= Void delete_file (fname: STRING) -- Remove file fname. require valid_str: fname /= Void; exists: is_file(fname); -- not is_open (fname) not_used: ensure done: last_success implies not is_file(fname) copy_file (orig_file, dest_file: STRING) -- Copy orig_file to dest_file. require valid_str: orig_file /= Void and dest_file /= Void; exists: is_file(orig_file); no_existing_dest: not is_file(dest_file) ensure done: last_success implies is_file(dest_file) move_file (orig_file, dest_file: STRING) -- Move orig_file to dest_file. require valid_str: orig_file /= Void and dest_file /= Void; exists: is_file(orig_file); no_existing_dest: not is_file(dest_file); -- not is_open (orig_name) not_used: ensure done: last_success implies is_file(dest_file) and not is_file(orig_file) feature(s) from F_FILE_SYSTEM -- Status last_success: BOOLEAN -- Was the last operation successful? last_size: INTEGER -- Result of last free_disk_space operation. require ok: last_success = true ensure done: Result >= 0 last_directory: STRING -- Result of last system directory request such -- as current_directory. require ok: last_success = true ensure done: Result /= Void last_content: DS_LIST[STRING] -- Result of last of directory_content. require ok: last_success = true ensure done: Result /= Void last_error: INTEGER -- Operating system last error code. require failed: last_success = false end of F_FILE_SYSTEM