indexing
description: "Defines the coordinates of the upper-left and lower-right corners of a rectangle."
status: "See notice at end of class."
date: "$Date$"
revision: "$Revision$"
class interface
WEL_RECT
create
make (a_left, a_top, a_right, a_bottom: INTEGER)
lefttop
rightbottoma_lefta_top
a_righta_bottom
ensure
left_set: left = a_left
top_set: top = a_top
right_set: right = a_right
bottom_set: bottom = a_bottom
make_by_pointer (a_pointer: POINTER)
itema_pointer
item
a_pointer
WEL_ANY
ensure WEL_ANY
item_set: item = a_pointer
shared: shared
make_client (window: WEL_WINDOW)
window
require
window_not_void: window /= void
window_exists: window.exists
ensure
left_equal_zero: left = 0
top_equal_zero: top = 0
client_rect_set: is_equal (window.client_rect)
make_window (window: WEL_WINDOW)
window
require
window_not_void: window /= void
window_exists: window.exists
ensure
window_rect_set: is_equal (window.window_rect)
feature
bottom: INTEGER
height: INTEGER
item: POINTER
WEL_ANY
left: INTEGER
WEL_RECTx
right: INTEGER
top: INTEGER
WEL_RECTy
width: INTEGER
x: INTEGER
WEL_RECTleft
y: INTEGER
WEL_RECTtop
feature
structure_size: INTEGER
ensure WEL_STRUCTURE
positive_result: Result > 0
feature
is_equal (other: like Current): BOOLEAN
Currentother
require ANY
other_not_void: other /= void
ensure ANY
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
feature
empty: BOOLEAN
exists: BOOLEAN
item
WEL_ANY
ensure WEL_ANY
Result = (item /= default_pointer)
point_in (point: WEL_POINT): BOOLEAN
point
require
point_not_void: point /= void
shared: BOOLEAN
item
item
destroy_item
item
WEL_ANY
feature
set_shared
shared
WEL_ANY
ensure WEL_ANY
shared: shared
set_unshared
shared
WEL_ANY
ensure WEL_ANY
unshared: not shared
feature
set_bottom (a_bottom: INTEGER)
bottoma_bottom
ensure
bottom_set: bottom = a_bottom
set_item (an_item: POINTER)
iteman_item
WEL_ANY
ensure WEL_ANY
item_set: item = an_item
set_left (a_left: INTEGER)
lefta_left
ensure
left_set: left = a_left
set_rect (a_left, a_top, a_right, a_bottom: INTEGER)
lefttoprightbottom
a_lefta_topa_righta_bottom
ensure
left_set: left = a_left
top_set: top = a_top
right_set: right = a_right
bottom_set: bottom = a_bottom
set_right (a_right: INTEGER)
righta_right
ensure
right_set: right = a_right
set_top (a_top: INTEGER)
topa_top
ensure
top_set: top = a_top
feature
dispose
Current
Current
WEL_ANY
feature
to_integer: INTEGER
item
WEL_ANY
ensure WEL_ANY
Result = cwel_pointer_to_integer (item)
feature
inflate (a_x, a_y: INTEGER)
a_xa_y
ensure
left_set: left = old left - a_x
top_set: top = old top - a_x
right_set: right = old right + a_y
bottom_set: bottom = old bottom + a_y
initialize
WEL_STRUCTURE
require WEL_STRUCTURE
exists: exists
initialize_with_character (a_character: CHARACTER)
a_character
WEL_STRUCTURE
require WEL_STRUCTURE
exists: exists
intersect (rect1, rect2: WEL_RECT)
rect1
rect2rect1rect2
empty
require
rect1_not_void: rect1 /= void
rect2_not_void: rect2 /= void
memory_copy (source_pointer: POINTER; length: INTEGER)
lengthsource_pointeritem
WEL_STRUCTURE
require WEL_STRUCTURE
length_small_enough: length <= structure_size
length_large_enough: length > 0
exists: exists
offset (a_x, a_y: INTEGER)
a_xa_y
ensure
x_set: x = old x + a_x
y_set: y = old y + a_y
right_set: right = old right + a_x
bottom_set: bottom = old bottom + a_y
subtract (rect1, rect2: WEL_RECT)
rect2rect1
require
rect1_not_void: rect1 /= void
rect2_not_void: rect2 /= void
union (rect1, rect2: WEL_RECT)
rect1rect2
require
rect1_not_void: rect1 /= void
rect2_not_void: rect2 /= void
invariant
positive_width: width >= 0
positive_height: height >= 0
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- WEL_RECT