+
Point of view
All features
class FILL_RECTANGLE
- width >= min_width or computing_size
- height >= min_height or computing_size
- std_width > 0
- std_height > 0
- not x_shrink_allowed implies width >= std_width or computing_size
- not x_expand_allowed implies width <= std_width or computing_size
- not y_shrink_allowed implies height >= std_height or computing_size
- not y_expand_allowed implies height <= std_height or computing_size
require
- x >= 0
- y >= 0
- w >= min_width
- h >= min_height
ensure
require
- w >= min_width
- h >= min_height
ensure
require
- p = Void implies parent /= Void
- p /= Void implies parent = Void
- p /= Void implies p.has_child(Current)
ensure
frozen
effective function
frozen
effective function
frozen
effective function
frozen
effective function
frozen
effective function
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
deep_sky_blue_color:
COLOR
once function
light_sky_blue_color:
COLOR
once function
light_steel_blue_color:
COLOR
once function
pale_turquoise_color:
COLOR
once function
dark_turquoise_color:
COLOR
once function
medium_turquoise_color:
COLOR
once function
yellow_green_color:
COLOR
once function
light_yellow_color:
COLOR
once function
light_salmon_color:
COLOR
once function
pale_violet_red_color:
COLOR
once function
medium_violet_red_color:
COLOR
once function
dark_magenta_color:
COLOR
once function
medium_purple_color:
COLOR
once function