Banded matrix Application Object

A Banded_matrix is a Table that has all its non-default terms in a (relatively small) number of consecutive diagonals.

EXPRESS specification:

*)
ENTITY Banded_matrix
  SUBTYPE OF (Table);
  default  :  Maths_value;
  below  :  INTEGER;
  above  :  INTEGER;
WHERE
   nondefault : -below <= above;
END_ENTITY;
(*

Attribute definitions:

default: The default value for locations outside the band.

below: The number of diagonals below the main diagonal which may contain non-default terms.

above: The number of diagonals above the main diagonal which may contain non-default terms.

Formal propositions:

nondefault: At least one diagonal must be permitted to have non-default entries.

NOTE - Negative values are allowed for the attributes below and above. A banded matrix in which all the non-default entries are in the first diagonal above the main diagonal can be represented efficiently using the value -1 for below and +1 for above.