class interface F_RANDOM_FILE

creation
   make
      --  Create a file object.


feature(s) from MEMORY
   --  Removal :

   dispose
      --  Close file handle.

      ensure
         done: handle = Invalid_handle_value

   full_collect
      --  Force a full collection cycle if garbage collection is
      --  enabled; do nothing otherwise.


feature(s) from F_STREAM
   --  Constant

   Byte_maximum: INTEGER

feature(s) from F_STREAM
   --  Access

   connect
      --  Open the file.

      ensure
         can_fail:  --  success implies is_alive

   imperative_connect
      --  Open the file and raise an exception if failed.

      ensure
         valid: is_alive

   disconnect
      --  Close the file 
      --  (REQUIRED in order to flush temporary buffers).

      require
         valid: is_alive
      ensure
         done: not is_alive

feature(s) from F_STREAM
   --  Status

   is_alive: BOOLEAN
      --  Is the file stream open? (validity and openess is the same 
      --  for this kind of stream).


   has_data: BOOLEAN
      --  Is at least one byte waiting to be read?

      require
         valid: is_alive

   has_error: BOOLEAN
      --  Has the stream got errors?


   is_readable: BOOLEAN
      --  Is the stream readable?


   is_writable: BOOLEAN
      --  Is the stream writable?


feature(s) from F_STREAM
   --  Read/write

   last_byte: INTEGER
      --  Last byte read.

      ensure
         byte_size: Result >= 0 and then Result <= Byte_maximum

   read_byte
      --  Read one byte and update last byte.

      require
         valid: is_alive;
         readable: is_readable;
         available: has_data

   write_byte (b: INTEGER)
      --  Write a byte.

      require
         valid: is_alive;
         writable: is_writable;
         byte_size: b >= 0 and then b <= Byte_maximum

feature(s) from F_FILE
   --  Assertions

   is_valid_name (str: STRING): BOOLEAN
      --  Is the string a valid (Win32) file name?

      require
         valid: str /= Void

feature(s) from F_FILE
   --  Access mode

   set_name (str: STRING)
      --  Set the file name.

      require
         closed: not is_alive;
         valid_string: str /= Void;
         valid_file_name: is_valid_name(str)

   set_mode_read
      --  Set mode to be read only (default).

      require
         closed: not is_alive

   reset_mode
      --  Set mode to be read only (default).

      require
         closed: not is_alive

   set_mode_write
      --  Set mode to write only.

      require
         closed: not is_alive

   set_mode_read_write
      --  Set mode to be read/write.

      require
         closed: not is_alive

   set_share_read
      --  Set sharing to read.

      require
         closed: not is_alive

   reset_share
      --  Set sharing mode to no sharing (default).

      require
         closed: not is_alive

   set_share_no
      --  Set sharing mode to no sharing (default).

      require
         closed: not is_alive

   reset_open
      --  Create new file or reset existing one.

      require
         closed: not is_alive; --  when is_writable
         relevant: 

   set_open_zero
      --  Create new file or reset existing one.

      require
         closed: not is_alive; --  when is_writable
         relevant: 

   set_open_new
      --  Create new file, fail if file exists.

      require
         closed: not is_alive; --  when is_writable
         relevant: 

   set_open_existing
      --  Open existing file only.

      require
         closed: not is_alive; --  when is_writable
         relevant: 

   set_open_replace
      --  Open existing file and truncate it, fail if there 
      --  is no existing file.

      require
         closed: not is_alive;
         writable: is_writable

   set_open_always
      --  Open existing file without changing it, or create 
      --  if no file exists.

      require
         closed: not is_alive; --  when is_writable
         relevant: 

feature(s) from F_FILE
   --  Access

   is_open: BOOLEAN
      --  Is the file stream open? (validity and openess is the same 
      --  for this kind of stream).


feature(s) from F_FILE
   --  Block

   write_block (memory: F_MEMORY)
      --  Write a memory block to disk.

      require
         alive: is_alive;
         writable: is_writable

   read_block (req_size: INTEGER)
      --  Read a fixed size block from stream.

      require
         size_ok: req_size > 0;
         alive: is_alive;
         readable: is_readable;
         waiting: has_data
      ensure
         block_of: not has_error implies last_block /= Void and then last_block.size = req_size

   last_block: F_MEMORY
      --  Last memory block read (new block for each read operation).


feature(s) from F_FINITE_STREAM
   --  Position

   set_position (idx: INTEGER)
      --  Set current position in stream.

      require
         alive: is_alive;
         valid_pos: idx >= 1 and idx <= size
      ensure
         done: not has_error implies position = idx

   position: INTEGER
      --  Current position in the stream.

      require
         alive: is_alive
      ensure
         bounds: position >= 1 and position <= size

   size: INTEGER
      --  Current size of stream in bytes.

      require
         alive: is_alive

invariant
   valid_index: buffer_index <= buffer_max;
   valid_buffer: is_alive implies buffer /= Void;

end of F_RANDOM_FILE