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

em.utility

Class EM_BINARY_RING_BUFFER


Direct ancestors

KI_BUFFER

Creation

Features

Invariants

indexing

description

binary ring buffer

date

$Date: 2005/10/26 17:11:18 $

revision

$Revision: 1.6 $

class

EM_BINARY_RING_BUFFER

inherit

KI_BUFFER

create

make (n: INTEGER)

-- Create a new binary ring buffer being able
-- to contain n characters.

require
n_not_negative: n >= 0
ensure
count_set: count = n

feature -- Access

item (i: INTEGER): CHARACTER

-- Item at position i

-- (From KI_BUFFER)

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

feature -- Measurement

count: INTEGER

-- Number of items in buffer

-- (From KI_BUFFER)

ensure
count_positive: Result >= 0
free: INTEGER

-- Number of free items in buffer

feature -- Element change

clear

-- fast clear buffer

fill_from_stream (a_stream: KI_INPUT_STREAM [CHARACTER]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.

-- (From KI_BUFFER)

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.

-- (From KI_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.

-- (From KI_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: CHARACTER; i: INTEGER)

-- Replace item at position i by v.

-- (From KI_BUFFER)

require
i_large_enough: i >= 1
i_small_enough: i <= count
ensure
inserted: item (i) = v
read_to (a_array: EM_INT8_ARRAY; nb: INTEGER): INTEGER

-- read from buffer to array at most nb items
-- returns the number of read items

require
a_array_not_void: a_array /= Void
nb_large_enough: nb > 0
nb_not_to_large: nb <= a_array.count
write_from_character_buffer (a_buffer: KI_CHARACTER_BUFFER)

-- Fill buffer from other buffer

require
a_buffer_not_void: a_buffer /= Void
enough_space: a_buffer.count <= free
write_from_stream (a_stream: KI_INPUT_STREAM [CHARACTER]; nb: INTEGER): INTEGER

-- Fill buffer, 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
nb_large_enough: nb > 0
enough_space: nb <= free

feature -- Resizing

resize (n: INTEGER)

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

-- (From KI_BUFFER)

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

invariant

mutex_exist: mutex /= Void
buffer_exist: buffer /= Void

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

end