class COLOR
Features exported to
ANY
Direct parents
non-conformant parents
ANY
Summary
creation features
like_rgb
(r:
REAL
, g:
REAL
, b:
REAL
)
like_rgb_8
(r:
INTEGER
, g:
INTEGER
, b:
INTEGER
)
like_rgb_16
(r:
INTEGER
, g:
INTEGER
, b:
INTEGER
)
exported features
red
:
INTEGER
green
:
INTEGER
blue
:
INTEGER
Details
like_rgb
(r:
REAL
, g:
REAL
, b:
REAL
)
require
r.in_range(0.0, 1.0)
g.in_range(0.0, 1.0)
b.in_range(0.0, 1.0)
like_rgb_8
(r:
INTEGER
, g:
INTEGER
, b:
INTEGER
)
require
r.in_range(0, 255)
g.in_range(0, 255)
b.in_range(0, 255)
like_rgb_16
(r:
INTEGER
, g:
INTEGER
, b:
INTEGER
)
require
r.in_range(0, 65535)
g.in_range(0, 65535)
b.in_range(0, 65535)
red
:
INTEGER
green
:
INTEGER
blue
:
INTEGER
Class invariant
red.in_range(0, 65535)
green.in_range(0, 65535)
blue.in_range(0, 65535)