deferred class FILE

Features exported to INTERNALS_HANDLER

Common parent class to all the file-related streams. Provides a common connection interface to the "real" files of the operating system.

Direct parents

non-conformant parents

ANY

Known children

conformant children

BINARY_FILE_READ, BINARY_FILE_WRITE, TEXT_FILE_READ, TEXT_FILE_READ_WRITE, TEXT_FILE_WRITE

Summary

exported features

Details

path: STRING

Not Void when connected to the corresponding file on the disk.

is_connected: BOOLEAN

Is this file connected to some file of the operating system?

ensure

  • definition: Result = (path /= Void)

deferred connect_to (new_path: STRING)

Try to connect to an existing file of the operating system.

require

  • not is_connected
  • not_malformed_path: not new_path.is_empty

ensure

  • is_connected implies path.same_as(new_path)

deferred disconnect

Disconnect from any file.

require

  • is_connected

ensure

  • not is_connected