Eiffel Media API
Overview Cluster Class Classes Index      Previous Next      Top Features

kernel.io

Class KI_BUFFER


Known direct descendants

EM_BINARY_RING_BUFFER, KI_CHARACTER_BUFFER

Features

Invariants

indexing

description

Interface for buffers

library

Gobo Eiffel Kernel Library

copyright

Copyright (c) 2001, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2004/11/14 15:09:42 $

revision

$Revision: 1.9 $

deferred class

KI_BUFFER [G]

feature -- Access

item (i: INTEGER): G

-- Item at position i

require
i_large_enough: i >= 1
i_small_enough: i <= count

feature -- Measurement

count: INTEGER

-- Number of items in buffer

ensure
count_positive: Result >= 0

feature -- Element change

fill_from_stream (a_stream: KI_INPUT_STREAM [G]; pos, nb: INTEGER): INTEGER

-- Fill buffer, starting at position pos, with
-- at most nb items read from a_stream.
-- Return the number of items actually read.

require
a_stream_not_void: a_stream /= Void
a_stream_open_read: a_stream.is_open_read
not_end_of_input: not a_stream.end_of_input
pos_large_enough: pos >= 1
nb_large_enough: nb > 0
enough_space: (pos + nb - 1) <= count
ensure
nb_item_read_large_enough: Result >= 0
nb_item_read_small_enough: Result <= nb
not_end_of_input: not a_stream.end_of_input implies Result > 0
move_left (old_pos, new_pos: INTEGER; nb: INTEGER)

-- Copy nb items from old_pos to
-- new_pos in buffer.

require
nb_positive: nb >= 0
old_pos_large_enough: old_pos >= 1
enough_characters: (old_pos + nb - 1) <= count
new_pos_large_enough: new_pos >= 1
enough_space: (new_pos + nb - 1) <= count
move_left: old_pos > new_pos
move_right (old_pos, new_pos: INTEGER; nb: INTEGER)

-- Copy nb items from old_pos to
-- new_pos in buffer.

require
nb_positive: nb >= 0
old_pos_large_enough: old_pos >= 1
enough_characters: (old_pos + nb - 1) <= count
new_pos_large_enough: new_pos >= 1
enough_space: (new_pos + nb - 1) <= count
move_right: old_pos < new_pos
put (v: G; i: INTEGER)

-- Replace item at position i by v.

require
i_large_enough: i >= 1
i_small_enough: i <= count
ensure
inserted: item (i) = v

feature -- Resizing

resize (n: INTEGER)

-- Resize buffer so that it contains n items.
-- Do not lose any previously entered items.

require
n_large_enough: n >= count
ensure
count_set: count = n

invariant

-- From ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)

end