Finite real interval Application Object

A Finite_real_interval is a Real_interval that has a lower and an upper bound.

EXPRESS specification:

*)
ENTITY Finite_real_interval
   SUBTYPE OF (Real_interval);
   lobnd : REAL;
   loclosure : BOOLEAN;
   hibnd : REAL;
   hiclosure : BOOLEAN;
WHERE
   nontrivial : lobnd < hibnd;
END_ENTITY;
(*

Attributes:

lobnd: The lower bound for the interval.

loclosure: Closure indicator that is as follows:

true

The interval includes reals greater than or equal to lobnd, i.e. the interval is closed below.

false

The interval includes reals greater than lobnd, i.e. the interval is open below.

hibnd: The upper bound for the interval.

hiclosure: Closure indicator that is as follows:

true

The interval includes reals less than or equal to hibnd, i.e. the interval is closed above.

false

The interval includes reals less than hibnd, i.e. the interval is open above.

Formal propositions:

nontrivial: The lower bound must be strictly less than the upper bound.