class interface DEVICE_CAPABILITIES feature(s) from DEVICE_CAPABILITIES -- Precondition is_device_ready: BOOLEAN -- Is the parent device valid? feature(s) from DEVICE_CAPABILITIES -- Device type is_plotter: BOOLEAN -- Is the device a plotter? require ready: is_device_ready is_raster_display: BOOLEAN -- Is the device a raster display? require ready: is_device_ready is_raster_printer: BOOLEAN -- Is the device a raster printer? require ready: is_device_ready is_raster_camera: BOOLEAN -- Is the device a raster camera? require ready: is_device_ready is_character_stream: BOOLEAN -- Is the device a character stream? require ready: is_device_ready is_metafile: BOOLEAN -- Is the device a metafile? require ready: is_device_ready is_display_file: BOOLEAN -- Is the device a display file? require ready: is_device_ready feature(s) from DEVICE_CAPABILITIES -- Device size and definition width_mm: INTEGER -- Width of the device screen (millimetres). require ready: is_device_ready height_mm: INTEGER -- Height of the device screen (millimetres). require ready: is_device_ready width_pixel: INTEGER -- Width of the device screen (pixels). require ready: is_device_ready height_pixel: INTEGER -- Height of the device screen (pixels). require ready: is_device_ready width_dpi: INTEGER -- Number of pixel per inch (dot-per-inch) along the horizontal axis. require ready: is_device_ready height_dpi: INTEGER -- Number of pixel per inch (dot-per-inch) along the vertical axis. require ready: is_device_ready screen_pixel: RECTANGLE -- Helper function providing rectangle of screen in pixels for -- window positioning, etc. require ready: is_device_ready ensure is_copy: Result /= Void feature(s) from DEVICE_CAPABILITIES -- Colors color_bits_per_pixel: INTEGER -- Number of adjacent colour bits for each pixel. require ready: is_device_ready color_plane: INTEGER -- Number of colour planes. require ready: is_device_ready color_number: INTEGER -- Number of colours currently available (typically 20 on screens). require ready: is_device_ready has_palette: BOOLEAN -- Is display palettised (or true colour)? require ready: is_device_ready palette_bits_per_pixel: INTEGER -- Actual colour resolution of a palettised device in bits per pixel. require ready: is_device_ready; palette: has_palette palette_reserved: INTEGER -- Number of reserved entries in the system palette. require ready: is_device_ready; palette: has_palette palette_size: INTEGER -- Nymber of entries in the system palette. require ready: is_device_ready; palette: has_palette feature(s) from DEVICE_CAPABILITIES -- Raster capabilities has_raster_bitmap: BOOLEAN -- Has raster capabilities? (pixel, bitmap transfer) require ready: is_device_ready feature(s) from DEVICE_CAPABILITIES -- Text capabilities can_rotate_text: BOOLEAN -- Can the device rotate text? require ready: is_device_ready can_rotate_text_90: BOOLEAN -- Can the device rotate text at 90, 180, 270 degrees? require ready: is_device_ready ensure implication: can_rotate_text invariant device_exist: parent /= Void; end of DEVICE_CAPABILITIES