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).

Version:

$Revision: 1.16 $

Author:

Marko van Dooren

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)
public behavior

pre elements != null;
pre elements.length > 0;

post getNbRows() == elements.length;
post isSquare();
post isDiagonal();
post (\forall int i; i>=0 && i elements[i] == elementAt(i+1,i+1)));
Initialize a new diagonal Matrix with the given array of diagonal element.

Matrix(double[][] elements)
public behavior

pre elements != null;
pre elements.length > 0;
pre (\exist int nbColumns; nbColumns > 0;
(\forall int i; i>=0 && i elements[i] != null &&
elements[i].length == nbColumns));

post getNbRows() == elements.length;
post getNbColumns() == elements[0].length;
post (\forall int i; i>=0 && i (\forall int j; j>=0 && j elements[i][j] == elementAt(i+1,j+1)));
Initialize a new Matrix from the given 2D array of doubles.

Matrix(int rows, int columns)
public invariant getNbDimensions() == 2;

public behavior

post getNbColumns() == columns;
post getNbRows() == rows;
post (\forall int i; i>0 && i < getNbRows();
(\forall int j; j > 0 && j < getNbColumns();
elementAt(i,j) == 0));
Initialize a new Matrix with the given number of rows and columns

Method Summary

void	add(Matrix other) public behavior pre other != null; pre sameDimensions(other); post (\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))); Add the given matrix to this matrix.
java.lang.Object	clone() public behavior post equals(\result); post \result instanceof Matrix; Return a clone
void	divide(double factor) public behavior post (\forall int i; i>=1 && i<= getNbRows(); (\forall int j; j>=1 && j<= getNbColumns(); elementAt(i,j) == \old(elementAt(i,j)) / factor)); Divide this matrix by a given factor.
double	elementAt(int[] index) pre validIndex(index); Return the element at the given index.
double	elementAt(int row, int column) public behavior pre validIndex(row, column); post elementAt({row, column}); Return the element at the given row and column.
boolean	equals(java.lang.Object other) public behavior post !(other instanceof Matrix) ==> false; post !(sameDimensions((Matrix)other)) ==> false; post (other instanceof Matrix) && (sameDimensions((Matrix)other)) ==> \result == (\forall int i; i>=1 i<=getNbRows(); (\forall int j; j>=1 j<=getNbColumns(); ((Matrix)\result).elementAt(i,j) == elementAt(i,j); post \result != this; Check whether the given object is equal to this matrix.
Column	getColumn(int index) public behavior pre index > 0 && index <= getNbColumns(); post \result != null; post \result.size() == getNbRows(); post (\forall int i; i>0 && i < getNbRows(); \result.elementAt(i) == elementAt(i,index)); Return the column with the given index.
int[]	getDimensions() post \result.length == getNbDimensions(); Return the dimensions of this matrix
int	getNbColumns() public behavior post \result == getDimensions()[1]; Return the number of columns of this matrix.
int	getNbDimensions() public invariant getDimensions().length == getNbDimensions(); public invariant (\forall int i; i>=0 && i getDimensions()[i] > 0); Return the number of dimensions of this matrix.
int	getNbRows() public behavior post \result == getDimensions()[0]; Return the number of rows of this matrix.
Row	getRow(int index) public behavior pre index > 0 && index <= getNbRows(); post \result != null; post \result.size() == getNbColumns(); post (\forall int i; i>0 && i < getNbColumns(); \result.elementAt(i) == elementAt(i,index)); Return the row with the given index.
boolean	isDiagonal() public behavior post \result == (\forall int i; i>=1 && i<=getNbRows(); (\forall int j; j>=1 && j<=getNbColumns(); (j != i) => elementAt(i,j) == 0)); Check whether or not this matrix is a diagonal matrix.
boolean	isLowerTriangular() public behavior post \result == (\forall int i; i>=1 && i<=getNbRows(); (\forall int j; j>=1 && j<=getNbColumns(); (i > j) => elementAt(i,j) == 0)); Check whether or not this matrix is lower triangular
boolean	isPermutationMatrix() post \result == isSquare() && // 1 non-zero element in each row (\forall int i; i>=1 && i<=getNbRows(); (\num_of int j; j>=1 && j<=getNbColumns() && elementAt(i,j) != 0;1) == 1) && // 1 non-zero element in each column (\forall int i; i>=1 && i<=getNbColumns(); (\num_of int j; j>=1 && j<=getNbRows() && elementAt(j,i) != 0;1) == 1) && // each element is 0 or 1 (\forall int i; i>=1 && i<=getNbRows(); (\forall int j; j>=1 && j<=getNbColumns(); elementAt(i,j) == 0 || elementAt(i,j) == 1)); Check whether or not this matrix is a permutation matrix.
boolean	isSquare() public behavior post getNbColumns() == getNbRows(); Check whether or not this matrix is square.
boolean	isSymmetric() public behavior post \result == isSquare() && (\forall int i; i>=1 && i<=getNbRows(); (\forall int j; j>=1 && j<=getNbColumns(); elementAt(i,j) == elementAt(j,i))); Check whether or not this matrix is symmetric.
boolean	isUpperTriangular() public behavior post \result == (\forall int i; i>=1 && i<=getNbRows(); (\forall int j; j>=1 && j<=getNbColumns(); (i < j) => elementAt(i,j) == 0)); Check whether or not this matrix is upper triangular
void	leftGivens(double c, double s, int i, int k) public behavior pre (1 <= i) && (i < k) && (k <= getNbRows()); post getColumn(i).equals(\old(getColumn(i).times(c).minus(getColumn(k).times(s)))); post getColumn(k).equals(\old(getColumn(i).times(s).plus(getColumn(k).times(c))));
Matrix	minus(Matrix other) public behavior pre other != null; pre sameDimensions(other); post \result != null; post \result.sameDimensions(this); post (\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))); Return a new matrix that equals this matrix minus the given matrix.
void	multiply(double factor) public behavior post (\forall int i; i>=1 && i<= getNbRows(); (\forall int j; j>=1 && j<= getNbColumns(); elementAt(i,j) == \old(elementAt(i,j)) * factor)); Multiply this matrix by a given factor.
Matrix	plus(Matrix other) public behavior pre other != null; pre sameDimensions(other); post \result != null; post \result.sameDimensions(this); post (\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))); Return a new matrix that is the sum of this matrix and the given matrix
Matrix	returnTranspose() public behavior post \result.sameDimensions(this); post (\forall int i; i>0 && i<= getNbRows(); (\forall int j; j>0 && j elementAt(i,j) == \result.elementAt(j,i))); Return the transpose of this matrix.
void	rightGivens(double c, double s, int i, int k) public behavior pre (1 <= i) && (i < k) && (k <= getNbColumns()); post getColumn(i).equals(\old(getColumn(i).times(c).minus(getColumn(k).times(s)))); post getColumn(k).equals(\old(getColumn(i).times(s).plus(getColumn(k).times(c))));
boolean	sameDimensions(Matrix other) public behavior pre other != null post getNbColumns() == other.getNbColumns(); post getNbRows() == other.getNbRows(); Check wether the given matrix has the same dimensions as this one.
void	setColumn(int i, Column column) public behavior pre i>=1 && i<=getNbColumns(); pre column != null; pre column.size() == getNbRows(); post getColumn(i).equals(column); Set the i-th column of this matrix
void	setElementAt(int[] index, double value) pre validIndex(index); post elementAt(index) == value; Set the element at the given index to the given value.
void	setElementAt(int row, int column, double value) public behavior pre validIndex(row, column); post elementAt(row, column) == value; Set the element at the given row and column to the given value.
void	setRow(int i, Row row) public behavior pre i>=1 && i<=getNbRows(); pre row != null; pre row.size() == getNbColumns(); post getRow(i).equals(row); Set the i-th row of this matrix
void	setSubMatrix(int row, int column, Matrix matrix) public behavior pre matrix != null; pre validIndex(row, column); pre validIndex(row + matrix.getNbRows() - 1, column + matrix.getNbColumns() - 1); post subMatrix(row, column, row + matrix.getNbRows() - 1, column + matrix.getNbColumns() - 1).equals(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) public behavior pre validIndex(x1, y1); pre validIndex(x2, y2); pre x2 >= x1; pre y2 >= y1; post \fresh(\result); post \result.getNbRows() == x2 - x1 + 1; post \result.getNbColumns() == y2 - y1 + 1; post (\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))); Return the submatrix starting from (x1,y1) to (x2,y2).
void	subtract(Matrix other) public behavior pre other != null; pre sameDimensions(other); post (\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))); Subtract the given matrix from this matrix.
Matrix	times(double factor) public behavior post \result != null; post \result.sameDimensions(this); post (\forall int i; i>=1 && i<= getNbRows(); (\forall int j; j>=1 && j<= getNbColumns(); \result.elementAt(i,j) == elementAt(i,j) * factor)); Return a matrix that equals this matrix times a given factor.
Matrix	times(Matrix other) public behavior pre other != null; pre other.getNbRows() == getNbColumns(); pre other.getNbColumns() == getNbRows(); post \result != null; post (\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)))); post \result.getNbRows() == getNbRows(); post \result.getNbColumns() == other.getNbColumns(); post \fresh(result); // MvDMvDMvD We should put this everywhere we return a matrix // since matrices are mutable.
java.lang.String	toString() see superclass
void	transpose() public behavior post getNbColumns() == \old(getNbRows()); post getNbRows() == \old(getNbColumns()); post (\forall int i; i>=1 && i<=getNbRows(); (\forall int j; j>=1 && j elementAt(i,j) == \old(elementAt(j,i)))); Transpose this matrix.
static Matrix	unity(int size) public behavior pre size > 0; post \fresh(\result); post \result.getNbRows() == size; post \result.getNbColumns() == size; post (\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))); Return a new unity matrix of the given size
boolean	validIndex(int row, int column) public behavior post \result == (row > 0) && (row <= getNbRows()) && (column > 0) && (column <= getNbColumns()); 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).

Constructor Detail

Matrix

public Matrix(int rows,
              int columns)

public invariant getNbDimensions() == 2;

public behavior

post getNbColumns() == columns;
post getNbRows() == rows;
post (\forall int i; i>0 && i < getNbRows();
(\forall int j; j > 0 && j < getNbColumns();
elementAt(i,j) == 0));
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.

Matrix

public Matrix(double[][] elements)

public behavior

pre elements != null;
pre elements.length > 0;
pre (\exist int nbColumns; nbColumns > 0;
(\forall int i; i>=0 && i elements[i] != null &&
elements[i].length == nbColumns));

post getNbRows() == elements.length;
post getNbColumns() == elements[0].length;
post (\forall int i; i>=0 && i (\forall int j; j>=0 && j elements[i][j] == elementAt(i+1,j+1)));
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.

Matrix

public Matrix(double[] elements)

public behavior

pre elements != null;
pre elements.length > 0;

post getNbRows() == elements.length;
post isSquare();
post isDiagonal();
post (\forall int i; i>=0 && i elements[i] == elementAt(i+1,i+1)));
Initialize a new diagonal Matrix with the given array of diagonal element.

Parameters:

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

Method Detail

unity

public static Matrix unity(int size)

public behavior

pre size > 0;

post \fresh(\result);
post \result.getNbRows() == size;
post \result.getNbColumns() == size;
post (\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)));
Return a new unity matrix of the given size

Parameters:

size - The number of rows/columns of the matrix

getNbDimensions

public int getNbDimensions()

Description copied from class: NMatrix

public invariant getDimensions().length == getNbDimensions();
public invariant (\forall int i; i>=0 && i getDimensions()[i] > 0);
Return the number of dimensions of this matrix.

Overrides:

getNbDimensions in class NMatrix

See Also:

superclass

getDimensions

public int[] getDimensions()

Description copied from class: NMatrix

post \result.length == getNbDimensions();
Return the dimensions of this matrix

Overrides:

getDimensions in class NMatrix

See Also:

superclass

getNbRows

public int getNbRows()

public behavior

post \result == getDimensions()[0];
Return the number of rows of this matrix.

getNbColumns

public int getNbColumns()

public behavior

post \result == getDimensions()[1];
Return the number of columns of this matrix.

elementAt

public double elementAt(int[] index)

Description copied from class: NMatrix

pre validIndex(index);
Return the element at the given index.

Overrides:

elementAt in class NMatrix

See Also:

superclass

elementAt

public double elementAt(int row,
                        int column)

public behavior

pre validIndex(row, column);

post elementAt({row, 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.

setElementAt

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

public behavior

pre validIndex(row, column);

post elementAt(row, column) == 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.

setElementAt

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

Description copied from class: NMatrix

pre validIndex(index);

post elementAt(index) == value;
Set the element at the given index to the given value.

Overrides:

setElementAt in class NMatrix

See Also:

superclass

validIndex

public boolean validIndex(int row,
                          int column)

public behavior

post \result == (row > 0) &&
(row <= getNbRows()) &&
(column > 0) &&
(column <= getNbColumns());
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.

getColumn

public Column getColumn(int index)

public behavior

pre index > 0 && index <= getNbColumns();

post \result != null;
post \result.size() == getNbRows();
post (\forall int i; i>0 && i < getNbRows();
\result.elementAt(i) == elementAt(i,index));
Return the column with the given index.

Parameters:

index - The index of the requested column.

setColumn

public void setColumn(int i,
                      Column column)

public behavior

pre i>=1 && i<=getNbColumns();
pre column != null;
pre column.size() == getNbRows();

post getColumn(i).equals(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

getRow

public Row getRow(int index)

public behavior

pre index > 0 && index <= getNbRows();

post \result != null;
post \result.size() == getNbColumns();
post (\forall int i; i>0 && i < getNbColumns();
\result.elementAt(i) == elementAt(i,index));
Return the row with the given index.

Parameters:

index - The index of the requested row.

setRow

public void setRow(int i,
                   Row row)

public behavior

pre i>=1 && i<=getNbRows();
pre row != null;
pre row.size() == getNbColumns();

post getRow(i).equals(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

add

public void add(Matrix other)

public behavior

pre other != null;
pre sameDimensions(other);

post (\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)));
Add the given matrix to this matrix.

Parameters:

other - The matrix to be added.

plus

public Matrix plus(Matrix other)

public behavior

pre other != null;
pre sameDimensions(other);

post \result != null;
post \result.sameDimensions(this);
post (\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)));
Return a new matrix that is the sum of this matrix and the given matrix

Parameters:

other - The matrix to be added.

subtract

public void subtract(Matrix other)

public behavior

pre other != null;
pre sameDimensions(other);

post (\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)));
Subtract the given matrix from this matrix.

Parameters:

other - The matrix to be added.

minus

public Matrix minus(Matrix other)

public behavior

pre other != null;
pre sameDimensions(other);

post \result != null;
post \result.sameDimensions(this);
post (\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)));
Return a new matrix that equals this matrix minus the given matrix.

Parameters:

other - The matrix to be added.

times

public Matrix times(Matrix other)

public behavior

pre other != null;
pre other.getNbRows() == getNbColumns();
pre other.getNbColumns() == getNbRows();

post \result != null;
post (\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))));
post \result.getNbRows() == getNbRows();
post \result.getNbColumns() == other.getNbColumns();
post \fresh(result);

// MvDMvDMvD We should put this everywhere we return a matrix
// since matrices are mutable. We don't want to change an existing one.
Right-multiply this matrix by another. \result = this * other

Parameters:

other - The matrix to multiply this matrix by.

times

public Matrix times(double factor)

public behavior

post \result != null;
post \result.sameDimensions(this);
post (\forall int i; i>=1 && i<= getNbRows();
(\forall int j; j>=1 && j<= getNbColumns();
\result.elementAt(i,j) == elementAt(i,j) * factor));
Return a matrix that equals this matrix times a given factor.

Parameters:

factor - The factor to multiply this matrix with.

multiply

public void multiply(double factor)

public behavior

post (\forall int i; i>=1 && i<= getNbRows();
(\forall int j; j>=1 && j<= getNbColumns();
elementAt(i,j) == \old(elementAt(i,j)) * factor));
Multiply this matrix by a given factor.

Parameters:

factor - The factor to multiply this matrix with.

divide

public void divide(double factor)

public behavior

post (\forall int i; i>=1 && i<= getNbRows();
(\forall int j; j>=1 && j<= getNbColumns();
elementAt(i,j) == \old(elementAt(i,j)) / factor));
Divide this matrix by a given factor.

Parameters:

factor - The factor to divide this matrix by.

transpose

public void transpose()

public behavior

post getNbColumns() == \old(getNbRows());
post getNbRows() == \old(getNbColumns());
post (\forall int i; i>=1 && i<=getNbRows();
(\forall int j; j>=1 && j elementAt(i,j) == \old(elementAt(j,i))));
Transpose this matrix.

leftGivens

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

public behavior

pre (1 <= i) && (i < k) && (k <= getNbRows());

post getColumn(i).equals(\old(getColumn(i).times(c).minus(getColumn(k).times(s))));
post getColumn(k).equals(\old(getColumn(i).times(s).plus(getColumn(k).times(c))));

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

rightGivens

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

public behavior

pre (1 <= i) && (i < k) && (k <= getNbColumns());

post getColumn(i).equals(\old(getColumn(i).times(c).minus(getColumn(k).times(s))));
post getColumn(k).equals(\old(getColumn(i).times(s).plus(getColumn(k).times(c))));

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

returnTranspose

public Matrix returnTranspose()

public behavior

post \result.sameDimensions(this);
post (\forall int i; i>0 && i<= getNbRows();
(\forall int j; j>0 && j elementAt(i,j) == \result.elementAt(j,i)));
Return the transpose of this matrix.

sameDimensions

public boolean sameDimensions(Matrix other)

public behavior

pre other != null

post getNbColumns() == other.getNbColumns();
post getNbRows() == other.getNbRows();
Check wether the given matrix has the same dimensions as this one.

Parameters:

other - The other matrix

subMatrix

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

public behavior

pre validIndex(x1, y1);
pre validIndex(x2, y2);
pre x2 >= x1;
pre y2 >= y1;

post \fresh(\result);
post \result.getNbRows() == x2 - x1 + 1;
post \result.getNbColumns() == y2 - y1 + 1;
post (\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)));
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.

setSubMatrix

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

public behavior

pre matrix != null;
pre validIndex(row, column);
pre validIndex(row + matrix.getNbRows() - 1, column + matrix.getNbColumns() - 1);

post subMatrix(row, column, row + matrix.getNbRows() - 1, column + matrix.getNbColumns() - 1).equals(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

isUpperTriangular

public boolean isUpperTriangular()

public behavior

post \result == (\forall int i; i>=1 && i<=getNbRows();
(\forall int j; j>=1 && j<=getNbColumns();
(i < j) => elementAt(i,j) == 0));
Check whether or not this matrix is upper triangular

isLowerTriangular

public boolean isLowerTriangular()

public behavior

post \result == (\forall int i; i>=1 && i<=getNbRows();
(\forall int j; j>=1 && j<=getNbColumns();
(i > j) => elementAt(i,j) == 0));
Check whether or not this matrix is lower triangular

isDiagonal

public boolean isDiagonal()

public behavior

post \result == (\forall int i; i>=1 && i<=getNbRows();
(\forall int j; j>=1 && j<=getNbColumns();
(j != i) => elementAt(i,j) == 0));
Check whether or not this matrix is a diagonal matrix.

toString

public java.lang.String toString()

see superclass

Overrides:

toString in class java.lang.Object

clone

public java.lang.Object clone()

public behavior

post equals(\result);
post \result instanceof Matrix;
Return a clone

Overrides:

clone in class java.lang.Object

equals

public boolean equals(java.lang.Object other)

public behavior

post !(other instanceof Matrix) ==> false;
post !(sameDimensions((Matrix)other)) ==> false;
post (other instanceof Matrix) && (sameDimensions((Matrix)other)) ==>
\result == (\forall int i; i>=1 i<=getNbRows();
(\forall int j; j>=1 j<=getNbColumns();
((Matrix)\result).elementAt(i,j) ==
elementAt(i,j);
post \result != this;
Check whether the given object is equal to this matrix.

Overrides:

equals in class java.lang.Object

isSquare

public boolean isSquare()

public behavior

post getNbColumns() == getNbRows();
Check whether or not this matrix is square.

isSymmetric

public boolean isSymmetric()

public behavior

post \result == isSquare() &&
(\forall int i; i>=1 && i<=getNbRows();
(\forall int j; j>=1 && j<=getNbColumns();
elementAt(i,j) == elementAt(j,i)));
Check whether or not this matrix is symmetric.

isPermutationMatrix

public boolean isPermutationMatrix()

post \result == isSquare() &&
// 1 non-zero element in each row
(\forall int i; i>=1 && i<=getNbRows();
(\num_of int j; j>=1 && j<=getNbColumns() && elementAt(i,j) != 0;1) == 1) &&
// 1 non-zero element in each column
(\forall int i; i>=1 && i<=getNbColumns();
(\num_of int j; j>=1 && j<=getNbRows() && elementAt(j,i) != 0;1) == 1) &&
// each element is 0 or 1
(\forall int i; i>=1 && i<=getNbRows();
(\forall int j; j>=1 && j<=getNbColumns();
elementAt(i,j) == 0 || elementAt(i,j) == 1));
Check whether or not this matrix is a permutation matrix.