expanded class RECT

Features exported to ANY

Describe rectangular area.

Direct parents

non-conformant parents

ANY

Summary

exported features

Details

x: INTEGER
y: INTEGER
width: INTEGER
height: INTEGER
make (new_x: INTEGER, new_y: INTEGER, new_width: INTEGER, new_height: INTEGER)

Initialize all values at the same time.

require

  • new_width >= 0
  • new_height >= 0

ensure

  • x = new_x
  • y = new_y
  • width = new_width
  • height = new_height

set_x (new_x: INTEGER)

ensure

  • x = new_x

set_y (new_y: INTEGER)

ensure

  • y = new_y

move_to (new_x: INTEGER, new_y: INTEGER)

Move the rectangle origin to (new_x, new_y) point.

ensure

  • x = new_x
  • y = new_y

offset (dx: INTEGER, dy: INTEGER)

Move the rectangle origin by dx and dy offsets (delta).

ensure

  • x = old x + dx
  • y = old y + dy

resize (new_width: INTEGER, new_height: INTEGER)

Change the rectangle size to new_width x new_height

require

  • new_width >= 0
  • new_height >= 0

ensure

  • width = new_width
  • height = new_height

inflate (dw: INTEGER, dh: INTEGER)

Change width by dw value and height by dh value (delta).

require

  • width + dw >= 0
  • height + dh >= 0

ensure

  • width = old width + dw
  • height = old height + dh

set_empty

ensure

  • width = 0
  • height = 0

is_empty: BOOLEAN

ensure

  • Result = (width = 0 or height = 0)

intersect (other: RECT): RECT

Return the area common to Current with other. Result width and height are 0 if intersect area is empty.

ensure

  • Result.width = 0 = (Result.height = 0)
  • Result.width = 0 implies Result.x = 0
  • Result.width = 0 implies Result.y = 0
  • (other.x < x + width and other.y < y + height and x < other.x + other.width and y < other.y + other.height) = (Result.width /= 0)

intersect_def (ox: INTEGER, oy: INTEGER, ow: INTEGER, oh: INTEGER): RECT

Same as intersect with other given by it's values rather than a RECT object.

require

  • ow >= 0
  • oh >= 0

ensure

  • Result.width = 0 = (Result.height = 0)
  • Result.width = 0 implies Result.x = 0
  • Result.width = 0 implies Result.y = 0
  • (ox < x + width and oy < y + height and x < ox + ow and y < oy + oh) = (Result.width /= 0)

union (other: RECT): RECT

Return the smallest rectangle containing Current and other.

ensure

  • Current.is_empty implies Result = other
  • not Current.is_empty and other.is_empty implies Result = Current
  • not Current.is_empty implies Result.intersect(Current) = Current
  • not other.is_empty implies Result.intersect(other) = other

contain (point_x: INTEGER, point_y: INTEGER): BOOLEAN

Does the point belongs to the rectangle?

ensure

  • Result = not Current.intersect_def(point_x, point_y, 1, 1).is_empty

include (point_x: INTEGER, point_y: INTEGER): BOOLEAN

Does the point belongs to the rectangle?

ensure

  • Result = not Current.intersect_def(point_x, point_y, 1, 1).is_empty

Class invariant