Finite integer interval Application Object

A Finite_integer_interval is an Integer_interval that has a lower and an upper bound.

*)
ENTITY Finite_integer_interval
  SUBTYPE OF (Integer_interval);
  size  : INTEGER;
  lobnd : INTEGER;
DERIVE
  hibnd : INTEGER := lobnd + size - 1;
WHERE
  positive_definite_size :  size > 0;
END_ENTITY;
(*

Attributes:

size: The number of integers which are members of the interval.

lobnd: The smallest integer in the interval.

hibnd: The largest integer in the interval.

Formal proposistions:

positive_definite_size: The size shall be greater than zero.