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