class interface F_FILE_PROPERTIES creation make -- Creation. feature(s) from F_FILE_PROPERTIES -- Status set_file (filename: STRING) -- Set the file (or directory) name. require valid: filename /= Void ensure done: -- is_valid if successful is_valid: BOOLEAN -- Are the properties current? feature(s) from F_FILE_PROPERTIES -- Properties file_size: INTEGER -- File size in bytes. require valid: is_valid; notdir: not is_directory; -- file_size_kb * 1024 < 2^Integer_bits overflow: ensure positive: Result >= 0 file_size_kb: INTEGER -- File size in kilobytes. require valid: is_valid; notdir: not is_directory creation_time: P_DATE_TIME -- Creation time of the file. require valid: is_valid last_access_time: P_DATE_TIME -- Last access time. This includes reading, writing, -- and executing for programs. require valid: is_valid last_write_time: P_DATE_TIME -- Last time the file was written. require valid: is_valid is_hidden: BOOLEAN -- Is this file hidden? require valid: is_valid is_read_only: BOOLEAN -- Is this file read-only (attribute only, security permission -- are not kept into account)? require valid: is_valid is_system: BOOLEAN -- Is this file used exclusively by the operating -- system? require valid: is_valid is_archive: BOOLEAN -- Is this file marked as archived? require valid: is_valid is_directory: BOOLEAN -- Is this object a directory? require valid: is_valid end of F_FILE_PROPERTIES