Class FILE

5.15 Class FILE

indexing

description: "Files viewed as persistent sequences of characters"

class interface

FILE

creation

make (fn: STRING)
        -- Create file object with fn as file name.
    require
        string_exists: fn /= Void; 
        string_not_empty: not fn.empty
    ensure
        file_named: name.is_equal (fn); 
        file_closed: is_closed

make_create_read_write (fn: STRING)
        -- Create file object with fn as file name
        -- and open file for both reading and writing; 
        -- create it if it does not exist.
    require
        string_exists: fn /= Void; 
        string_not_empty: not fn.empty
    ensure
        exists: exists; 
        open_read: is_open_read; 
        open_write: is_open_write

make_open_append (fn: STRING)
        -- Create file object with fn as file name
        -- and open file in append-only mode.
    require
        string_exists: fn /= Void; 
        string_not_empty: not fn.empty
    ensure
        exists: exists; 
        open_append: is_open_append

make_open_read (fn: STRING)
        -- Create file object with fn as file name
        -- and open file in read mode.
    require
        string_exists: fn /= Void; 
        string_not_empty: not fn.empty
    ensure
        exists: exists; 
        open_read: is_open_read

make_open_read_write (fn: STRING)
        -- Create file object with fn as file name
        -- and open file for both reading and writing.
    require
        string_exists: fn /= Void; 
        string_not_empty: not fn.empty
    ensure
        exists: exists; 
        open_read: is_open_read; 
        open_write: is_open_write

make_open_write (fn: STRING)
        -- Create file object with fn as file name
        -- and open file for writing; 
        -- create it if it does not exist.
    require
        string_exists: fn /= Void; 
        string_not_empty: not fn.empty
    ensure
        exists: exists; 
        open_write: is_open_write

feature -- Access

name: STRING
        -- File name

feature -- Measurement

count: INTEGER
        -- Size in bytes (0 if no associated physical file)

feature -- Status report

empty: BOOLEAN
        -- Is structure empty?

end_of_file: BOOLEAN
        -- Has an EOF been detected?
    require
        opened: not is_closed

exists: BOOLEAN
        -- Does physical file exist?

is_closed: BOOLEAN
        -- Is file closed?

is_open_read: BOOLEAN
        -- Is file open for reading?

is_open_write: BOOLEAN
        -- Is file open for writing?

is_plain_text: BOOLEAN
        -- Is file reserved for text (character sequences)?

is_readable: BOOLEAN
        -- Is file readable?
    require
        handle_exists: exists

is_writable: BOOLEAN
        -- Is file writable?
    require
        handle_exists: exists

last_character: CHARACTER
        -- Last character read by read_character

last_double: DOUBLE
        -- Last double read by read_double

last_integer: INTEGER
        -- Last integer read by read_integer

last_real: REAL
        -- Last real read by read_real

last_string: STRING
        -- Last string read by read_line, 
        -- read_stream, or read_word

feature -- Status setting

close
        -- Close file.
    require
        medium_is_open: not is_closed
    ensure
        is_closed: is_closed

open_read
        -- Open file in read-only mode.
    require
        is_closed: is_closed
    ensure
        exists: exists;
        open_read: is_open_read

open_read_append
        -- Open file in read and write-at-end mode; 
        -- create it if it does not exist.
    require
        is_closed: is_closed
    ensure
        exists: exists;
        open_read: is_open_read
        open_append: is_open_append

open_read_write
        -- Open file in read and write mode.
    require
        is_closed: is_closed
    ensure
        exists: exists;
        open_read: is_open_read;
        open_write: is_open_write

open_write
        -- Open file in write-only mode; 
        -- create it if it does not exist.
    ensure
        exists: exists;
        open_write: is_open_write

feature -- Cursor movement

to_next_line
        -- Move to next input line.
    require
        readable: is_readable

feature -- Element change

change_name (new_name: STRING)
        -- Change file name to new_name
    require
        not_new_name_void: new_name /= Void; 
        file_exists: exists
    ensure
        name_changed: name.is_equal (new_name)

feature -- Removal

delete
        -- Remove link with physical file; delete physical
        -- file if no more link.
    require
        exists: exists

dispose
        -- Ensure this medium is closed when garbage-collected.

feature -- Input

read_character
        -- Read a new character.
        -- Make result available in last_character.
    require
        readable: is_readable

read_double
        -- Read the ASCII representation of a new double
        -- from file. Make result available in last_double.
    require
        readable: is_readable

read_integer
        -- Read the ASCII representation of a new integer
        -- from file. Make result available in last_integer.
    require
        readable: is_readable

read_line
        -- Read a string until new line or end of file.
        -- Make result available in laststring.
        -- New line will be consumed but not part of last_string.
    require
        readable: is_readable

read_real
        -- Read the ASCII representation of a new real
        -- from file. Make result available in last_real.
    require
        readable: is_readable

read_stream (nb_char: INTEGER)
        -- Read a string of at most nb_char bound characters
        -- or until end of file.
        -- Make result available in last_string.
    require
        readable: is_readable

read_word
        -- Read a new word from standard input.
        -- Make result available in last_string.

feature -- Output

put_boolean (b: BOOLEAN)
        -- Write ASCII value of b at current position.
    require
        extendible: extendible

put_character (c: CHARACTER)
        -- Write c at current position.
    require
        extendible: extendible

put_double (d: DOUBLE)
        -- Write ASCII value of d at current position.
    require
        extendible: extendible

put_integer (i: INTEGER)
        -- Write ASCII value of i at current position.
    require
        extendible: extendible

put_real (r: REAL)
        -- Write ASCII value of r at current position.
    require
        extendible: extendible

put_string (s: STRING)
        -- Write s at current position.
    require
        extendible: extendible

invariant

name_exists: name /= Void; 
name_not_empty: not name.empty; 
writable_if_extendible: extendible implies is_writable

end