indexing

	description: "Contiguous bytes of memory not managed by the Eiffel runtime."

class interface

	MEMORY_BLOCK

creation

	allocate,
	make_from_pointer

feature {NONE} -- Initialization

	allocate (size: INTEGER)
			-- Allocate `size' bytes of memory
		require
			positive_size: size > 0
		ensure
			owned: owner
			empty_block: empty

	make_from_pointer (location: POINTER; size: INTEGER)
			-- Point Current to `location' with capacity `size'.
		require
			pointer_not_null: a_pointer /= default_pointer
			positive_size: size > 0
		ensure
			not_owned: not owner
			empty_block: empty

feature -- Access

	item: POINTER
			-- Access to allocated memory.

	peek_character (index: INTEGER): CHARACTER is
			-- Character at location `index'.
		require
			valid_index: valid_index (index)

	peek_integer_8 (index: INTEGER): INTEGER_8 is
			-- 8-bit integer at location `index'.
		require
			valid_index: valid_index (index)

	peek_integer_16 (index: INTEGER): INTEGER_16 is
			-- 16-bit integer at location `index' in platform byte order.
		require
			valid_range: valid_index (index) and valid_index (index + 1)

	peek_integer_32 (index: INTEGER): INTEGER is
			-- 32-bit integer at location `index' in platform byte order.
		require
			valid_range: valid_index (index) and valid_index (index + 3)

	peek_integer_64 (index: INTEGER): INTEGER_64 is
			-- 64-bit integer at location `index' in platform byte order.
		require
			valid_range: valid_index (index) and valid_index (index + 7)

	peek_string (index: INTEGER; size: INTEGER): STRING is
			-- String of length `size' beginning at location `index'
		require
			valid_range: valid_index (index) and valid_index (index + size)
		ensure
			result_exists: Result /= Void
			count_consistent: Result.count = size

feature -- Access: Little-endian byte order

	peek_integer_16_le (index: INTEGER): INTEGER_16 is
			-- 16-bit integer at location `index' in little-endian byte order.
		require
			valid_range: valid_index (index) and valid_index (index + 1)

	peek_integer_32_le (index: INTEGER): INTEGER is
			-- 32-bit integer at location `index' in little-endian byte order.
		require
			valid_range: valid_index (index) and valid_index (index + 3)

	peek_integer_64_le (index: INTEGER): INTEGER_64 is
			-- 64-bit integer at location `index' in little-endian byte order.
		require
			valid_range: valid_index (index) and valid_index (index + 7)

feature -- Access: Big-endian (Network) byte order

	peek_integer_16_be (index: INTEGER): INTEGER_16 is
			-- 16-bit integer at location `index' in big-endian byte order.
		require
			valid_range: valid_index (index) and valid_index (index + 1)

	peek_integer_32_be (index: INTEGER): INTEGER is
			-- 32-bit integer at location `index' in big-endian byte order.
		require
			valid_range: valid_index (index) and valid_index (index + 3)

	peek_integer_64_be (index: INTEGER): INTEGER_64 is
			-- 64-bit integer at location `index' in big-endian byte order.
		require
			valid_range: valid_index (index) and valid_index (index + 7)

feature -- Measurement

	capacity: INTEGER
			-- Number of bytes Current can hold.

	count: INTEGER
			-- Number of zero-indexed, contiguous bytes containing information.

feature -- Status report

	empty: BOOLEAN
			-- Is block empty?

	owner: BOOLEAN
			-- Will `item' be deallocated when Current is collected?

	valid_index (i: INTEGER): BOOLEAN
			-- Can `size' bytes be read from or written to location `i'?
		ensure
			not_negative: Result implies i >= 0

feature -- Element change

	set_count (newcount: INTEGER)
			-- Change `count' to `newcount' bytes.
		require
			valid_count: 0 <= newcount and newcount <= capacity
		ensure
			count_set: count = newcount

	poke_character (index: INTEGER; value: CHARACTER) is
			-- Place character `value' into location `index'
		require
			valid_index: valid_index (index)

	poke_integer_8 (index: INTEGER; value: INTEGER_8) is
			-- Place 8-bit `value' into location `index'
		require
			valid_index: valid_index (index)

	poke_integer_16 (index: INTEGER; value: INTEGER_16) is
			-- Place 16-bit `value' into location `index' in platform byte order.
		require
			valid_range: valid_index (index) and valid_index (index + 1)

	poke_integer_32 (index: INTEGER; value: INTEGER) is
			-- Place 32-bit `value' into location `index' in platform byte order.
		require
			valid_range: valid_index (index) and valid_index (index + 3)

	poke_integer_64 (index: INTEGER; value: INTEGER_64) is
			-- Place 64-bit `value' into location `index' in platform byte order.
		require
			valid_range: valid_index (index) and valid_index (index + 7)

	poke_string (index: INTEGER; value: STRING) is
			-- Place `value' into location `index'
		require
			value_exists: value /= Void
			valid_range: valid_index (index) and valid_index (index + value.count)

feature -- Element change: Little-endian byte order

	poke_integer_16_le (index: INTEGER; value: INTEGER_16) is
			-- Place 16-bit `value' into location `index' in little-endian byte order
		require
			valid_range: valid_index (index) and valid_index (index + 1)

	poke_integer_32_le (index: INTEGER; value: INTEGER) is
			-- Place 32-bit `value' into location `index' in little-endian byte order
		require
			valid_range: valid_index (index) and valid_index (index + 3)

	poke_integer_64_le (index: INTEGER; value: INTEGER_64) is
			-- Place 64-bit `value' into location `index' in little-endian byte order
		require
			valid_range: valid_index (index) and valid_index (index + 7)

feature -- Element change: Big-endian (Network) byte order

	poke_integer_16_be (index: INTEGER; value: INTEGER_16) is
			-- Place 16-bit `value' into location `index' in big-endian byte order
		require
			valid_range: valid_index (index) and valid_index (index + 1)

	poke_integer_32_be (index: INTEGER; value: INTEGER) is
			-- Place 32-bit `value' into location `index' in big-endian byte order
		require
			valid_range: valid_index (index) and valid_index (index + 3)

	poke_integer_64_be (index: INTEGER; value: INTEGER_64) is
			-- Place 64-bit `value' into location `index' in big-endian byte order
		require
			valid_range: valid_index (index) and valid_index (index + 7)

feature -- Removal

	clear
			-- Set all bytes to zero and reset `count'.
		ensure
			empty_block: empty

	dispose
			-- Reclaim `item' when `owner'.
		ensure
			reset_when_owned: owner implies (item = default_pointer)

feature -- Resizing

	resize (newsize: INTEGER)
			-- Re-allocate block to fit `newsize' bytes.
		require
			owned: owner
			positive_size: newsize > 0
		ensure
			new_capacity: capacity = newsize

	expand (amount: INTEGER)
			-- Expand memory block to accomodate `amount' more bytes.
			-- Do not corrupt previously allocated memory.
		require
			owned: owner
			positive_amount: amount > 0
		ensure
			new_capacity: capacity = old capacity + amount

invariant

	consistent_count: 0 <= count and count <= capacity
	positive_capacity: capacity > 0
	item_not_null: item /= default_pointer

end