5.15 Class FILE PreviousNext

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

Copyright 1995, Nonprofit International Consortium for Eiffel
mailto:
nice@atlanta.twr.com
Last Updated: 26 October 1997

HomeTocPreviousNext