indexing
	description: "A data packet for sending and receiving on a socket."
	status: "See notice at end of class"
	date: "$Date$"
	revision: "$Revision$"

class interface
	PACKET

create 

	make (size: INTEGER)
			-- Create a packet.
		require
			valid_size: size >= 0

feature -- Initialization

	make (size: INTEGER)
			-- Create a packet.
		require
			valid_size: size >= 0
	
feature -- Access

	data: SPECIAL [CHARACTER]
			-- Special data zone
			-- (from TO_SPECIAL)

	element (pos: INTEGER): CHARACTER
			-- Element at position pos
		require
			pos_valid: valid_position (pos)
	
feature -- Measurement

	count: INTEGER
			-- Number of elements in packet
	
feature -- Comparison

	is_equal (other: like Current): BOOLEAN
			-- Is current packet equal to other?
		require -- from ANY
			other_not_void: other /= void
		ensure -- from ANY
			symmetric: Result implies other.is_equal (Current)
			consistent: standard_is_equal (other) implies Result
	
feature -- Status report

	valid_position (pos: INTEGER): BOOLEAN
			-- Is position pos valid for this packet?
	
feature -- Element change

	put_element (an_item: CHARACTER; pos: INTEGER)
			-- Put element an_item at position pos.
			-- Fist element has position 0.
		require
			pos_valid: valid_position (pos)
	
feature -- Duplication

	copy (other: like Current)
			-- Reinitialize by copying characters of other.
			-- (This is also used by clone)
		require -- from ANY
			other_not_void: other /= void
			type_identity: same_type (other)
		ensure -- from ANY
			is_equal: is_equal (other)
		ensure then
			size_valid: count = other.count
	
invariant

	data_not_equal_void: data /= void
		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)

end -- class PACKET