Sparse matrix Application Object

A Sparse_matrix is a Table in which most terms have a default value.

The attributes of this Application Object specify the non-default terms. The attributes list the non-zero positions and their corresponding values, ordered and indexed in a manner which supports efficient searching.

To evaluate the sparse matrix for the position [j,k] when order is row by row:

1. evaluate index at position j to obtain m_lo;
2. evaluate index at position (j+1) to obtain m_hi;
3. search locations at positions m_lo <=m < m_hi looking for the entry k;
4. if evaluation of locations at position m returns k,
   • evaluate terms at position m to obtain the sparse matrix entry for position [j,k],
   otherwise (k not an entry in locations in the computed interval),
   • the sparse matrix entry for position [j,k] is default.

If the order is by columns, then the roles of j and k are reversed.

EXPRESS specification:

*)
ENTITY Sparse_matrix
  SUBTYPE OF (Table);
  default    :  Maths_value;
  index      :  LIST [1,?] OF INTEGER;
  locations  :  LIST [1,?] OF INTEGER;
WHERE
  matrix : SIZEOF(SELF\table.shape) = 2;
  proper_index_length:
    (order AND (SIZEOF(index) =  self\table.shape[1] + 1))
     OR
    ((NOT order) AND (SIZEOF(index) = self\table.shape[2] + 1));
  proper_locations_length: SIZEOF(locations) = SIZEOF(terms);
END_ENTITY;
(*

Attribute definitions:

default: The default value for locations not specified by index and locations.

index: The integer tuple providing starting locations in location and terms for the non-zero elements in each row (if order is true) or column (if order is false).

locations: The integer tuple providing the column indices of the non-default positions (if order is true) or the row indices of the non-default positions (if order is false) in the order determined for the non-zero positions by order.

SELF/table.terms: The values of the non-default terms in one-to-one correspondence with locations.

Formal propositions:

matrix: The shape of the table shall be two dimensional.

proper_index_length: If order is row by row, then the domain of index is the space of row positions of the matrix plus an extra row, and if order is column by column, then the domain of index is the space of column positions of the matrix plus an extra column.

proper_locations length: The length locations list must be the same as the length of the terms list.

Informal propositions:

proper_index_values: The values from index shall be in the range 1 to (SIZEOF(loc) + 1).

proper_locations_values: If order is row by row then the values from locations must be column positions of the matrix, and if order is column by column then the values from locations must be row positions.