class interface F_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). invariant valid_index: buffer_index <= buffer_max; valid_buffer: is_alive implies buffer /= Void; end of F_FILE