class interface ICO_HEADER creation make (a_block: F_MEMORY) -- Set associated memory block. require not_void: a_block /= Void feature(s) from ICO_HEADER -- Memory make (a_block: F_MEMORY) -- Set associated memory block. require not_void: a_block /= Void feature(s) from ICO_HEADER -- Memory set (a_block: F_MEMORY) -- Set associated memory block. require not_void: a_block /= Void feature(s) from ICO_HEADER -- Operation(s) is_valid: BOOLEAN -- Check layout. count: INTEGER -- Number of entries. require valid: is_valid entry (n: INTEGER): ICO_ENTRY -- Entry block. require valid: is_valid; min: n >= 1; max: n <= count ensure not_void: Result /= Void has_bitmap (an_entry: ICO_ENTRY): BOOLEAN -- Is there a bitmap pointed to by that entry. require valid: is_valid; not_void: an_entry /= Void bitmap (an_entry: ICO_ENTRY): ICO_BITMAP -- Bitmap corresponding to an entry. require valid: is_valid; not_void: an_entry /= Void; has_bitmap: has_bitmap(an_entry) ensure not_void: Result /= Void invariant valid_memory: memory /= Void; end of ICO_HEADER