org.jutil.math.matrix
Class Matrix

java.lang.Object
  |
  +--org.jutil.math.matrix.NMatrix
        |
        +--org.jutil.math.matrix.Matrix

Direct Known Subclasses:

Column, Row

public class Matrix

extends NMatrix

A class of 2D matrices. This version doesn't try that hard to perform stable calculations. If you need that, use the non-existing nummath package. If you don't know what it means, use this version :) Matrix also doesn't report any overflow (standard Java behavior).

Class Specifications

public invariant getNbDimensions() == 2;

Specifications inherited from class NMatrix

public invariant getDimensions().length == getNbDimensions(); public invariant ( \forall int i; i >= 0&&i < getNbDimensions(); getDimensions()[i] > 0);

Field Summary
static java.lang.String	CVS_REVISION           MvDMvDMvD : some operations don't have 2 sensible names for use as a mutator and inspector.

 

Constructor Summary

Matrix(double[] elements)           Initialize a new diagonal Matrix with the given array of diagonal element.

Matrix(double[][] elements)           Initialize a new Matrix from the given 2D array of doubles.

Matrix(int rows, int columns)           Initialize a new Matrix with the given number of rows and columns

 

Method Summary
void	add(Matrix other)           Add the given matrix to this matrix.
java.lang.Object	clone()           Return a clone
void	divide(double factor)           Divide this matrix by a given factor.
double	elementAt(int row, int column)           Return the element at the given row and column.
double	elementAt(int[] index)
boolean	equals(java.lang.Object other)           Check whether the given object is equal to this matrix.
Column	getColumn(int index)           Return the column with the given index.
int[]	getDimensions()
int	getNbColumns()           Return the number of columns of this matrix.
int	getNbDimensions()
int	getNbRows()           Return the number of rows of this matrix.
Row	getRow(int index)           Return the row with the given index.
boolean	isDiagonal()           Check whether or not this matrix is a diagonal matrix.
boolean	isLowerTriangular()           Check whether or not this matrix is lower triangular
boolean	isPermutationMatrix()           Check whether or not this matrix is a permutation matrix.
boolean	isSquare()           Check whether or not this matrix is square.
boolean	isSymmetric()           Check whether or not this matrix is symmetric.
boolean	isUpperTriangular()           Check whether or not this matrix is upper triangular
void	leftGivens(double c, double s, int i, int k)           Perform a givens rotation on this matrix from the left side with the givens matrix defined by c, s, i and k as follows (m = getNbRows()). 1 i k m 1 1 .
Matrix	minus(Matrix other)           Return a new matrix that equals this matrix minus the given matrix.
void	multiply(double factor)           Multiply this matrix by a given factor.
Matrix	plus(Matrix other)           Return a new matrix that is the sum of this matrix and the given matrix
Matrix	returnTranspose()           Return the transpose of this matrix.
void	rightGivens(double c, double s, int i, int k)           Perform a givens rotation on this matrix from the right side with the givens matrix defined by c, s, i and k as follows (n = getNbColumns()). 1 i k n 1 1 .
boolean	sameDimensions(Matrix other)           Check wether the given matrix has the same dimensions as this one.
void	setColumn(int i, Column column)           Set the i-th column of this matrix
void	setElementAt(int row, int column, double value)           Set the element at the given row and column to the given value.
void	setElementAt(int[] index, double value)
void	setRow(int i, Row row)           Set the i-th row of this matrix
void	setSubMatrix(int row, int column, Matrix matrix)           Replace a submatrix of this matrix with the given matrix at the given coordinates.
Matrix	subMatrix(int x1, int y1, int x2, int y2)           Return the submatrix starting from (x1,y1) to (x2,y2).
void	subtract(Matrix other)           Subtract the given matrix from this matrix.
Matrix	times(double factor)           Return a matrix that equals this matrix times a given factor.
Matrix	times(Matrix other)           Right-multiply this matrix by another.
java.lang.String	toString()           see superclass
void	transpose()           Transpose this matrix.
static Matrix	unity(int size)           Return a new unity matrix of the given size
boolean	validIndex(int row, int column)           Check whether or not the given row and column point to a valid position for this Matrix.

 

Methods inherited from class org.jutil.math.matrix.NMatrix

validIndex

 

Methods inherited from class java.lang.Object

finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

 

Field Detail

CVS_REVISION

public static final java.lang.String CVS_REVISION

MvDMvDMvD : some operations don't have 2 sensible names for use as a mutator and inspector. At this moment, I see have 3 possible naming schemes for tranformations on 2D matrices. 1) name() : a mutator which applies the tranformation to this matrix. if you want a clone, just make it yourself. 2) name() : an inspector which returns a new matrix nameThis() : a mutator which applies the tranformation to this matrix. 3) returnName() : an inspector which returns a new matrix name() : a mutator which applies the tranformation to this matrix. Personally, I like 3) the best. It feels like talking to a matrix. If you say "matrix.transpose" it will transpose itself.If you say "matrix.returnTranspose", it will return a transpose (a new matrix).

Matrix

public Matrix(int rows,
              int columns)

Initialize a new Matrix with the given number of rows and columns

Parameters:

columns - The number of columns for the new Matrix.

rows - The number of rows for the new Matrix.

Specifications:

public behavior
ensures getNbColumns() == columns;
ensures getNbRows() == rows;
ensures ( \forall int i; i > 0&&i < getNbRows(); ( \forall int j; j > 0&&j < getNbColumns(); elementAt(i,j) == 0));

Matrix

public Matrix(double[][] elements)

Initialize a new Matrix from the given 2D array of doubles.

Parameters:

elements - A 2D array containing the elements of the new Matrix. The first dimension is for the rows, the second for the columns.

Specifications:

public behavior
requires elements != null;
requires elements.length > 0;
requires ( \exists int nbColumns; nbColumns > 0; ( \forall int i; i >= 0&&i < elements.length; elements[i] != null&&elements[i].length == nbColumns));
ensures getNbRows() == elements.length;
ensures getNbColumns() == elements[0].length;
ensures ( \forall int i; i >= 0&&i < elements.length; ( \forall int j; j >= 0&&j < elements[0].length; elements[i][j] == elementAt(i+1,j+1)));

Matrix

public Matrix(double[] elements)

Initialize a new diagonal Matrix with the given array of diagonal element.

Parameters:

elements - An array containing the diagonal elements of the new Matrix.

Specifications:

public behavior
requires elements != null;
requires elements.length > 0;
ensures getNbRows() == elements.length;
ensures isSquare();
ensures isDiagonal();
ensures ( \forall int i; i >= 0&&i < elements.length; elements[i] == elementAt(i+1,i+1));

unity

public static Matrix unity(int size)

Return a new unity matrix of the given size

Parameters:

size - The number of rows/columns of the matrix

Specifications:

public behavior
requires size > 0;
ensures \fresh(\result );
ensures \result .getNbRows() == size;
ensures \result .getNbColumns() == size;
ensures ( \forall int i; i >= 1&&i <= size; ( \forall int j; j >= 1&&j <= size; ((i == j) ==> \result .elementAt(i,j) == 1)&&((i != j) ==> \result .elementAt(i,j) == 0)));

getNbDimensions

public int getNbDimensions()

See Also:

superclass

Specifications inherited from overridden method in class NMatrix:
      --- None ---

getDimensions

public int[] getDimensions()

See Also:

superclass

Specifications inherited from overridden method in class NMatrix:

ensures \result .length == getNbDimensions();

getNbRows

public int getNbRows()

Return the number of rows of this matrix.

Specifications:

public behavior
ensures \result == getDimensions()[0];

getNbColumns

public int getNbColumns()

Return the number of columns of this matrix.

Specifications:

public behavior
ensures \result == getDimensions()[1];

elementAt

public double elementAt(int[] index)

See Also:

superclass

Specifications inherited from overridden method in class NMatrix:

requires validIndex(index);

elementAt

public double elementAt(int row,
                        int column)

Return the element at the given row and column.

Parameters:

row - The row of the element to be retrieved.

column - The column of the element to be retrieved.

Specifications:

public behavior
requires validIndex(row,column);
ensures \result == elementAt( new int []{ row, column});

setElementAt

public void setElementAt(int row,
                         int column,
                         double value)

Set the element at the given row and column to the given value.

Parameters:

row - The row of the element to be retrieved.

column - The column of the element to be retrieved.

value - The new value for the element at the given row and column.

Specifications:

public behavior
requires validIndex(row,column);
ensures elementAt(row,column) == value;

setElementAt

public void setElementAt(int[] index,
                         double value)

See Also:

superclass

Specifications inherited from overridden method in class NMatrix:

requires validIndex(index);
ensures elementAt(index) == value;

validIndex

public boolean validIndex(int row,
                          int column)

Check whether or not the given row and column point to a valid position for this Matrix.

Parameters:

row - The row of the position.

column - The row of the position.

Specifications:

public behavior
ensures \result == (row > 0)&&(row <= getNbRows())&&(column > 0)&&(column <= getNbColumns());

getColumn

public Column getColumn(int index)

Return the column with the given index.

Parameters:

index - The index of the requested column.

Specifications:

public behavior
requires index > 0&&index <= getNbColumns();
ensures \result != null;
ensures \result .size() == getNbRows();
ensures ( \forall int i; i > 0&&i < getNbRows(); \result .elementAt(i) == elementAt(i,index));

setColumn

public void setColumn(int i,
                      Column column)

Set the i-th column of this matrix

Parameters:

i - The index of the column to be set.

column - The column which will be the new i-th column of this matrix

Specifications:

public behavior
requires i >= 1&&i <= getNbColumns();
requires column != null;
requires column.size() == getNbRows();
ensures getColumn(i).equals(column);

getRow

public Row getRow(int index)

Return the row with the given index.

Parameters:

index - The index of the requested row.

Specifications:

public behavior
requires index > 0&&index <= getNbRows();
ensures \result != null;
ensures \result .size() == getNbColumns();
ensures ( \forall int i; i > 0&&i < getNbColumns(); \result .elementAt(i) == elementAt(index,i));

setRow

public void setRow(int i,
                   Row row)

Set the i-th row of this matrix

Parameters:

i - The index of the row to be set.

column - The row which will be the new i-th row of this matrix

Specifications:

public behavior
requires i >= 1&&i <= getNbRows();
requires row != null;
requires row.size() == getNbColumns();
ensures getRow(i).equals(row);

add

public void add(Matrix other)

Add the given matrix to this matrix.

Parameters:

other - The matrix to be added.

Specifications:

public behavior
requires other != null;
requires sameDimensions(other);
ensures ( \forall int i; i >= 1&&i <= getNbRows(); ( \forall int j; j >= 1&&j <= getNbColumns(); elementAt(i,j) == \old(elementAt(i,j))+other.elementAt(i,j)));

plus

public Matrix plus(Matrix other)

Return a new matrix that is the sum of this matrix and the given matrix

Parameters:

other - The matrix to be added.

Specifications:

public behavior
requires other != null;
requires sameDimensions(other);
ensures \result != null;
ensures \result .sameDimensions(this);
ensures ( \forall int i; i >= 1&&i <= getNbRows(); ( \forall int j; j >= 1&&j <= getNbColumns(); \result .elementAt(i,j) == elementAt(i,j)+other.elementAt(i,j)));

subtract

public void subtract(Matrix other)

Subtract the given matrix from this matrix.

Parameters:

other - The matrix to be added.

Specifications:

public behavior
requires other != null;
requires sameDimensions(other);
ensures ( \forall int i; i >= 1&&i <= getNbRows(); ( \forall int j; j >= 1&&j <= getNbColumns(); elementAt(i,j) == \old(elementAt(i,j))-other.elementAt(i,j)));

minus

public Matrix minus(Matrix other)

Return a new matrix that equals this matrix minus the given matrix.

Parameters:

other - The matrix to be added.

Specifications:

public behavior
requires other != null;
requires sameDimensions(other);
ensures \result != null;
ensures \result .sameDimensions(this);
ensures ( \forall int i; i >= 1&&i <= getNbRows(); ( \forall int j; j >= 1&&j <= getNbColumns(); \result .elementAt(i,j) == elementAt(i,j)-other.elementAt(i,j)));

times

public Matrix times(Matrix other)

Right-multiply this matrix by another. \result = this * other

Parameters:

other - The matrix to multiply this matrix by.

Specifications:

public behavior
requires other != null;
requires other.getNbRows() == getNbColumns();
requires other.getNbColumns() == getNbRows();
ensures \result != null;
ensures ( \forall int i; i >= 1&&i <= getNbRows(); ( \forall int j; j >= 1&&j <= other.getNbColumns(); \result .elementAt(i,j) == ( \sum int k; k >= 1&&k <= getNbColumns(); elementAt(i,k)*other.elementAt(k,j))));
ensures \result .getNbRows() == getNbRows();
ensures \result .getNbColumns() == other.getNbColumns();
ensures \fresh(\result );

times

public Matrix times(double factor)

Return a matrix that equals this matrix times a given factor.

Parameters:

factor - The factor to multiply this matrix with.

Specifications:

public behavior
ensures \result != null;
ensures \result .sameDimensions(this);
ensures ( \forall int i; i >= 1&&i <= getNbRows(); ( \forall int j; j >= 1&&j <= getNbColumns(); \result .elementAt(i,j) == elementAt(i,j)*factor));

multiply

public void multiply(double factor)

Multiply this matrix by a given factor.

Parameters:

factor - The factor to multiply this matrix with.

Specifications:

public behavior
ensures ( \forall int i; i >= 1&&i <= getNbRows(); ( \forall int j; j >= 1&&j <= getNbColumns(); elementAt(i,j) == \old(elementAt(i,j))*factor));

divide

public void divide(double factor)

Divide this matrix by a given factor.

Parameters:

factor - The factor to divide this matrix by.

Specifications:

public behavior
ensures ( \forall int i; i >= 1&&i <= getNbRows(); ( \forall int j; j >= 1&&j <= getNbColumns(); elementAt(i,j) == \old(elementAt(i,j))/factor));

transpose

public void transpose()

Transpose this matrix.

Specifications:

public behavior
ensures getNbColumns() == \old(getNbRows());
ensures getNbRows() == \old(getNbColumns());
ensures ( \forall int i; i >= 1&&i <= getNbRows(); ( \forall int j; j >= 1&&j < getNbColumns(); elementAt(i,j) == \old(elementAt(j,i))));

leftGivens

public void leftGivens(double c,
                       double s,
                       int i,
                       int k)

Perform a givens rotation on this matrix from the left side with the givens matrix defined by c, s, i and k as follows (m = getNbRows()).

     1       i       k       m
 
 1   1 . . . 0 . . . 0 . . . 0
     . .     . .     . .     .
     .   .   .   .   .   .   .
     .     . .     . .     . .
 i   0 . . . c . . . s . . . 0
     . .     . .     . .     .
     .   .   .   .   .   .   .
     .     . .     . .     . .
 k   0 . . .-s . . . c . . . 0
     . .     . .     . .     .
     .   .   .   .   .   .   .
     .     . .     . .     . .
 m   0 . . . 0 . . . 0 . . . 1
 

This matrix (A) will be transformed into G*A.

Parameters:

c - The value of c

c - The value of s

i - The value of i

k - The value of k

Specifications:

public behavior
requires (1 <= i)&&(i < k)&&(k <= getNbRows());
ensures getColumn(i).equals(\old(getColumn(i).times(c).minus(getColumn(k).times(s))));
ensures getColumn(k).equals(\old(getColumn(i).times(s).plus(getColumn(k).times(c))));

rightGivens

public void rightGivens(double c,
                        double s,
                        int i,
                        int k)

Perform a givens rotation on this matrix from the right side with the givens matrix defined by c, s, i and k as follows (n = getNbColumns()).

     1       i       k       n
 
 1   1 . . . 0 . . . 0 . . . 0
     . .     . .     . .     .
     .   .   .   .   .   .   .
     .     . .     . .     . .
 i   0 . . . c . . . s . . . 0
     . .     . .     . .     .
     .   .   .   .   .   .   .
     .     . .     . .     . .
 k   0 . . .-s . . . c . . . 0
     . .     . .     . .     .
     .   .   .   .   .   .   .
     .     . .     . .     . .
 n   0 . . . 0 . . . 0 . . . 1
 

This matrix (A) will be transformed into A*G.

Parameters:

c - The value of c

c - The value of s

i - The value of i

k - The value of k

Specifications:

public behavior
requires (1 <= i)&&(i < k)&&(k <= getNbColumns());
ensures getColumn(i).equals(\old(getColumn(i).times(c).minus(getColumn(k).times(s))));
ensures getColumn(k).equals(\old(getColumn(i).times(s).plus(getColumn(k).times(c))));

returnTranspose

public Matrix returnTranspose()

Return the transpose of this matrix.

Specifications:

public behavior
ensures \result .sameDimensions(this);
ensures ( \forall int i; i > 0&&i <= getNbRows(); ( \forall int j; j > 0&&j < getNbColumns(); elementAt(i,j) == \result .elementAt(j,i)));

sameDimensions

public boolean sameDimensions(Matrix other)

Check wether the given matrix has the same dimensions as this one.

Parameters:

other - The other matrix

Specifications:

public behavior
requires other != null;
ensures getNbColumns() == other.getNbColumns();
ensures getNbRows() == other.getNbRows();

subMatrix

public Matrix subMatrix(int x1,
                        int y1,
                        int x2,
                        int y2)

Return the submatrix starting from (x1,y1) to (x2,y2).

Parameters:

x1 - The row from which to start.

y1 - The column from which to start.

x2 - The end row.

y2 - The end column.

Specifications:

public behavior
requires validIndex(x1,y1);
requires validIndex(x2,y2);
requires x2 >= x1;
requires y2 >= y1;
ensures \fresh(\result );
ensures \result .getNbRows() == x2-x1+1;
ensures \result .getNbColumns() == y2-y1+1;
ensures ( \forall int i; i >= x1&&i <= x2; ( \forall int j; j >= y1&&j <= y2; \result .elementAt(i-x1+1,j-y1+1) == elementAt(i,j)));

setSubMatrix

public void setSubMatrix(int row,
                         int column,
                         Matrix matrix)

Replace a submatrix of this matrix with the given matrix at the given coordinates.

Parameters:

row - The row of the top-left element of the submatrix that will be replaced.

column - The column of the top-left element of the submatrix that will be replaced.

matrix - The matrix to put into this matrix

Specifications:

public behavior
requires matrix != null;
requires validIndex(row,column);
requires validIndex(row+matrix.getNbRows()-1,column+matrix.getNbColumns()-1);
ensures subMatrix(row,column,row+matrix.getNbRows()-1,column+matrix.getNbColumns()-1).equals(matrix);

isUpperTriangular

public boolean isUpperTriangular()

Check whether or not this matrix is upper triangular

Specifications:

public behavior
ensures \result == ( \forall int i; i >= 1&&i <= getNbRows(); ( \forall int j; j >= 1&&j <= getNbColumns(); (i < j) ==> elementAt(i,j) == 0));

isLowerTriangular

public boolean isLowerTriangular()

Check whether or not this matrix is lower triangular

Specifications:

public behavior
ensures \result == ( \forall int i; i >= 1&&i <= getNbRows(); ( \forall int j; j >= 1&&j <= getNbColumns(); (i > j) ==> elementAt(i,j) == 0));

isDiagonal

public boolean isDiagonal()

Check whether or not this matrix is a diagonal matrix.

Specifications:

public behavior
ensures \result == ( \forall int i; i >= 1&&i <= getNbRows(); ( \forall int j; j >= 1&&j <= getNbColumns(); (j != i) ==> elementAt(i,j) == 0));

toString

public java.lang.String toString()

see superclass

clone

public java.lang.Object clone()

Return a clone

Specifications:

     also

public behavior
ensures equals(\result );
ensures \result instanceof Matrix;

equals

public boolean equals(java.lang.Object other)

Check whether the given object is equal to this matrix.

Specifications:

     also

public behavior
ensures !(other instanceof Matrix) ==> false;
ensures !(sameDimensions((Matrix)other)) ==> false;
ensures (other instanceof Matrix)&&(sameDimensions((Matrix)other)) ==> \result == ( \forall int i; i >= 1&&i <= getNbRows(); ( \forall int j; j >= 1&&j <= getNbColumns(); ((Matrix)other).elementAt(i,j) == elementAt(i,j)));

isSquare

public boolean isSquare()

Check whether or not this matrix is square.

Specifications:

public behavior
ensures getNbColumns() == getNbRows();

isSymmetric

public boolean isSymmetric()

Check whether or not this matrix is symmetric.

Specifications:

public behavior
ensures \result == isSquare()&&( \forall int i; i >= 1&&i <= getNbRows(); ( \forall int j; j >= 1&&j <= getNbColumns(); elementAt(i,j) == elementAt(j,i)));

isPermutationMatrix

public boolean isPermutationMatrix()

Check whether or not this matrix is a permutation matrix.

Specifications:

ensures \result == isSquare()&&( \forall int i; i >= 1&&i <= getNbRows(); ( \num_of int j; j >= 1&&j <= getNbColumns(); elementAt(i,j) != 0) == 1)&&( \forall int i; i >= 1&&i <= getNbColumns(); ( \num_of int j; j >= 1&&j <= getNbRows(); elementAt(j,i) != 0) == 1)&&( \forall int i; i >= 1&&i <= getNbRows(); ( \forall int j; j >= 1&&j <= getNbColumns(); elementAt(i,j) == 0||elementAt(i,j) == 1));