ELKS 95: Class FILE

This site contains older material on Eiffel. For the main Eiffel page, see http://www.eiffel.com.

Table of Contents Previous Chapter

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

Table of Contents Next Chapter

© 1985-2012 Eiffel Software. All rights reserved. -- Privacy Policy