+
Point of view
All features
deferred class IMAGE
- 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
-
valid_index: i.in_range(0, count - 1)
require
- x >= 0
- y >= 0
- 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
ensure
-
good_hash_value: Result >= 0
require
ensure
- Result implies hash_code = other.hash_code
-
commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)