class interface ICO_ENTRY creation make (a_block: F_MEMORY) require not_void: a_block /= Void feature(s) from ICO_ENTRY -- Creation make (a_block: F_MEMORY) require not_void: a_block /= Void feature(s) from ICO_ENTRY -- Creation set (a_block: F_MEMORY) require not_void: a_block /= Void feature(s) from ICO_ENTRY -- Operation(s) is_valid: BOOLEAN -- Layout OK? width: INTEGER -- Cursor width. require valid: is_valid height: INTEGER -- Cursor height. require valid: is_valid color_count: INTEGER -- Color count (2,16,256) require valid: is_valid bit_count: INTEGER -- Number of bit per pixel. require valid: is_valid size_in_bytes: INTEGER -- Size in bytes of image data. require valid: is_valid file_offset: INTEGER -- File offset. require valid: is_valid invariant block_not_void: memory /= Void; end of ICO_ENTRY