A B C D E F G H I J L M N O P Q R S T U V Z

A

ABSTRACT_FILTER - Static variable in class org.jutil.java.reflect.Methods

AbstractRevision - class org.jutil.junit.AbstractRevision.

A class that implements the non-basic methods of Revision.

AbstractRevision() - Constructor for class org.jutil.junit.AbstractRevision

AbstractSolver - class org.jutil.math.matrix.AbstractSolver.

A helper class for classes that solve systems of equations using matrices.

AbstractSolver() - Constructor for class org.jutil.math.matrix.AbstractSolver

accumulate(Collection) - Method in class org.jutil.java.collections.Accumulator

public behavior

pre (\forall Object o, collection.contains(o); isValidElement(o));

post (* the result of the accumulation is returned *);
post collection == null => \result == initialAccumulator();

signals (ConcurrentModificationException) (* The collection was modified while accumulating *);

accumulate(Object, boolean) - Method in class org.jutil.java.collections.BooleanAccumulator

public behavior

pre isValidElement(element);

accumulate(Object, boolean) - Method in class org.jutil.java.collections.ForAll

also public behavior

post \result == (acc && criterion(element));

accumulate(Object, boolean) - Method in class org.jutil.java.collections.Exists

also public behavior

post \result == acc || criterion(element);

accumulate(Object, int) - Method in class org.jutil.java.collections.IntegerAccumulator

// The given element may not be null
pre element != null;

accumulate(Object, int) - Method in class org.jutil.java.collections.Counter

also public behavior

// If the element satisfies the criterion, acc + 1 is returned to
// indicate 1 more element satisfies the criterion.
// otherwise acc is returned.
post criterion(element) == false ==> \result == acc;
post criterion(element) == true ==> \result == acc + 1;

accumulate(Object, Object) - Method in class org.jutil.java.collections.Accumulator

public behavior

pre isValidElement(element);

Accumulator - class org.jutil.java.collections.Accumulator.

A class of objects that accumulate over a collection.

Accumulator() - Constructor for class org.jutil.java.collections.Accumulator

add(ApplicabilityNotifier) - Method in class org.jutil.event.ChainNotifier

public behavior
assignable notifiers if notifier != null;
post notifier != null ==>
notifiers.equals(\old(notifiers.insertBack(notifier)));
Appends the specified element to the end of this list.

add(EventListener) - Method in class org.jutil.event.EventSourceSupport

public behavior
pre listener != null ==> isValidListener(listener);
assignable listeners;
// The given Listener is now in the set of listeners, if it is not null.
post listener != null ==> listeners.equals(\old(listeners.insert(listener)));
ensures_redundantly listener != null ==> listeners.has(listener);
Add an event Listener to the listeners to be notified by this.

add(int, ApplicabilityNotifier) - Method in class org.jutil.event.ChainNotifier

public behavior
assignable notifiers if notifier != null;
post notifier != null ==>
notifiers.equals(\old(notifiers.
insertBeforeIndex(index, notifier)));
signals (IndexOutOfBoundsException)
(index < 0) || (index >= notifiers.length());
Inserts the specified element at the specified position in this list.

add(Matrix) - Method in class org.jutil.math.matrix.Matrix

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.

add(Object) - Method in class org.jutil.java.collections.SkipListPQ

See superclass.

add(Object) - Method in class org.jutil.java.collections.SkipList

See superclass

add(Object) - Method in interface org.jutil.java.collections.PriorityQueue

public behavior

pre element != null;

post nbExplicitOccurrences(element) == \old(nbExplicitOccurrences(element)) + 1;
Add the given object to this PriorityQueue.

add(Object) - Method in class org.jutil.java.collections.BinomialHeap

See superclass.

add(Object) - Method in class org.jutil.java.collections.Singleton

also public behavior

post false;
exception UnsupportedOperationException true;
See superclass

add(StructureElement) - Method in class org.jutil.structure.StructureSet

public behavior

pre element != null;

post element.getStructuredSet() == this;
post \old(element.getStructuredSet()) != null &&
\old(element.getStructuredSet()) != this ==>
! \old(element.getStructuredSet()).contains(element);
post contains(element);
Remove the given StructureElement from this StructureSet.

addAll(Collection) - Method in class org.jutil.java.collections.Singleton

also public behavior

post false;
exception UnsupportedOperationException true;
See superclass

AndFilter - class org.jutil.java.collections.AndFilter.

The effect of this filter is the same as of a filter with the conjunction of the criteria of the filters it was build with.

AndFilter(Filter[]) - Constructor for class org.jutil.java.collections.AndFilter

public behavior

// The given array of filters may not be null.
pre filters != null;
// The given array may only contain effective Filter objects
pre (\forall int i; (i>=0) && (i
// The filters of this AndFilter are set to the given filters.
post Arrays.equals(getFilters(),filters);

ApplicabilityNotifier - interface org.jutil.event.ApplicabilityNotifier.

Instances of this type add the posibility for users to ask whether the instance is applicable to a given listener/event combination.

applyFromTo(Collection, Collection) - Method in class org.jutil.java.collections.Mapping

public behavior

pre (\forall Object o, fromCollection.contains(o); isValidElement(o));

// The elements are mapped into according to the
// mapping under public Object mapping(Object).
post (\forall Object o; fromCollection.contains(o);
\result.contains(mapping(o))) &&
(\forall Object o; toCollection.contains(o);
(\exists Object o2; fromCollection.contains(o2);
o.equals(mapping(o2))));
// is changed and returned
post \result == toCollection;

signals (ConcurrentModificationException) (* The collection was modified while mapping *);

applyTo(Collection) - Method in class org.jutil.java.collections.RobustVisitor

public behavior

pre (\forall Object o, collection.contains(o); isValidElement(o));

// The changes are applied to the given collection,
// which is returned afterwards
post \result == collection;
// public void visit(Object) is called for all
// elements of .
post (* for all e in collection: visit(e) *);

signals (ConcurrentModificationException) (* The collection was modified while visiting.

applyTo(Collection) - Method in class org.jutil.java.collections.Mapping

public behavior

pre (\forall Object o, collection.contains(o); isValidElement(o));

// The elements of the given set are replaced by their mapping under
// public Object mapping(Object).
post (\forall Object o; collection.contains(o);
\result.contains(mapping(o))) &&
(\forall Object o; \result.contains(o);
(\exists Object o2; collection.contains(o2);
mapping(o2).equals(o)));
post collection.size() == \old(collection.size());
// The given collection is changed and returned
post \result == collection;

signals (ConcurrentModificationException) (* The collection was modified while mapping *);

applyTo(Collection) - Method in class org.jutil.java.collections.Visitor

public behavior

pre (\forall Object o, collection.contains(o); isValidElement(o));

// The changes are applied to the given collection,
// which is returned afterwards
post \result == collection;

// public void visit(Object) is called for all elements.
post (* for all e in collection: visit(e) *);

signals (ConcurrentModificationException)
(* The collection was modified while calculating the tranitive closure.

applyTo(Enumeration) - Method in class org.jutil.java.collections.RobustVisitor

pre (* The enumeration must be at the beginning of its enumeration.

applyTo(Enumeration) - Method in class org.jutil.java.collections.Visitor

pre (* The enumeration must be at the beginning of its enumeration.

applyTo(Iterator) - Method in class org.jutil.java.collections.RobustVisitor

pre (* The iterator must be at the beginning of its iteration.

applyTo(Iterator) - Method in class org.jutil.java.collections.Visitor

pre (* The iterator must be at the beginning of its iteration.

applyTo(Map) - Method in class org.jutil.java.collections.MapVisitor

public behavior

pre (\forall Map.Entry entry; map.entrySet().contains(entry);
isValidPair(entry.getKey(), entry.getValue()));

// code>public void visit(Object) is called for all elements of

applyTo(Map) - Method in class org.jutil.java.collections.RobustMapVisitor

public behavior

pre (\forall Map.Entry entry; map.entrySet().contains(entry);
isValidPair(entry.getKey(), entry.getValue()));

// The changes are applied to the given set and it is returned afterwards.
post \result == map;
post (* public void visit(Object) is called for all elements of

applyTo(Object[]) - Method in class org.jutil.java.collections.RobustVisitor

// The changes are applied to the given array,
// which is returned afterwards
post \result == array;
// public void visit(Object) is called for all
// elements of .
post (* for all e in collection: visit(e) *);

signals (Exception)
(* Something has gone wrong during the visit *);

applyTo(Object[]) - Method in class org.jutil.java.collections.Visitor

// The changes are applied to the given object array,
// which is returned afterwards
post \result == array;

areInSamePackage(Class, Class) - Static method in class org.jutil.java.reflect.Classes

// The types to compare are not null.
pre (t1 != null) && (t2 != null);

// The result is true if the 2 given classes are defined
// in the same package.

ArrayCursor - class org.jutil.java.collections.ArrayCursor.

A class of objects that point to a certain index in a multi-dimensional array.

ArrayCursor(Object[]) - Constructor for class org.jutil.java.collections.ArrayCursor

// An ArrayCursor can not have null as dimensions.
public invariant getDimensions() != null;

// Dimensions can only have positive sizes.
public invariant (\forall int i; i >= 0 && i getDimensions()[i] > 0);

// The dimensions of a cursor are the dimension of its array.
public invariant getDimensions().equals(Arrays.getArrayDimensions(array));

// An ArrayCursor can not have null as cursor.
public invariant getCursor() != null;

// The cursor of an ArrayCursor has the same number of elements as
// there are dimensions
public invariant getCursor().length == getDimensions().length;

// An ArrayCursor can only point to a valid index for the
// represented array
public invariant (\forall int i; i >= 0 && i (getCursor()[i] >= 0) && (getCursor()[i] < getDimensions()[i]));

public model Object[] array;

// may not be null.
pre array != null;

// The dimensions of the new ArrayCursor are set to the
// dimensions of .
post getDimensions().equals(Arrays.getArrayDimensions(theArray));
// The array of this ArrayCursor is set to
post array == theArray;
Initialize a new ArrayCursor for a given array of objects.

Arrays - class org.jutil.java.collections.Arrays.

A class with static methods for arrays

Arrays() - Constructor for class org.jutil.java.collections.Arrays

asList(Throwable) - Static method in class org.jutil.java.throwable.StackTrace

pre t != null;

// The result is not null.
// The result does not contain null references.
post (\result != null) &&
(\forall Object o;\result.contains(o); o != null) &&
(\forall Object o;\result.contains(o); o instanceof String);

atEnd() - Method in class org.jutil.java.collections.ObjectArrayIterator

Check whether this iterator is positioned at the end of its array Result True if this iterator is positioned at the end of its array, false otherwise.

atEnd() - Method in class org.jutil.java.collections.ArrayCursor

// True if the elements in the cursor are equal to
// the maximum size of their dimension - 1 or if
// at least 1 dimension has size 0
post \result == (\forall int i; i>=0 && i < getCursor().length;
getCursor()[i]==getDimensions()[i]-1) ||
(\exists int i; i>=0 && i < getDimensions().length;
getDimensions()[i]==0);
Check whether this cursor points to the end of the array.

atStart() - Method in class org.jutil.java.collections.ObjectArrayIterator

Check whether this iterator is positioned at the beginning of its array Result True if this iterator is positioned at the beginning of its array, false otherwise.

atStart() - Method in class org.jutil.java.collections.ArrayCursor

// True if the cursor only contains 0's.
post \result == (\forall int i; i>=0 && i < getCursor().length;
getCursor()[i]==0);
Check whether this cursor points to the beginning of the array.

B

backSubstitute(Matrix, Column) - Method in class org.jutil.math.matrix.AbstractSolver

public behavior

pre R != null;
pre b != null;
pre R.isSquare();
pre R.isUpperTriangular;
pre b.size() == R.getNbRows();
pre (* R is nonsingular *);

post (* R.times(\result).equals(b) *);

BinomialHeap - class org.jutil.java.collections.BinomialHeap.

A BinomialHeap is a Heap that consists of a forest of Binomial Trees.

BinomialHeap(Comparator) - Constructor for class org.jutil.java.collections.BinomialHeap

public behavior

pre comparator != null;

post getComparator() == comparator;
post size() == 0;
Initialize a new BinomialHeap with the given comparator.

BinomialHeap(Comparator, Object) - Constructor for class org.jutil.java.collections.BinomialHeap

public behavior

pre comparator != null;
pre element != null;

post getComparator() == comparator;
post nbExplicitOccurrences(element) == 1;
post size() == 1;
Initialize a new BinomialHeap with the given comparator and element.

BlockingFifoList - class org.jutil.java.collections.BlockingFifoList.

Synchronized fifo list that will block the request to pop the first object until a first object is present.

BlockingFifoList() - Constructor for class org.jutil.java.collections.BlockingFifoList

public behavior

post size() == 0;
Initialize a new empty blocking fifo list.

BooleanAccumulator - class org.jutil.java.collections.BooleanAccumulator.

A boolean accumulator for collections.

BooleanAccumulator() - Constructor for class org.jutil.java.collections.BooleanAccumulator

C

ChainNotifier - class org.jutil.event.ChainNotifier.

ChainNotifier() - Constructor for class org.jutil.event.ChainNotifier

public behavior
assignable notifiers;
post notifiers.isEmpty();

CholeskyDecomposer - interface org.jutil.math.matrix.CholeskyDecomposer.

A class of objects that compute the Cholesky factorization of a symmetric matrix.

CholeskyDecomposition - interface org.jutil.math.matrix.CholeskyDecomposition.

This class represents a Cholesky factorization of a symmetric matrix.

Classes - class org.jutil.java.reflect.Classes.

Utility methods for class reflection.

Classes() - Constructor for class org.jutil.java.reflect.Classes

clear() - Method in class org.jutil.java.collections.SkipListPQ

See superclass.

clear() - Method in class org.jutil.java.collections.SkipList

See superclass

clear() - Method in interface org.jutil.java.collections.PriorityQueue

public behavior

post isEmpty();
Remove all elements.

clear() - Method in class org.jutil.java.collections.FifoList

See superclass/

clear() - Method in class org.jutil.java.collections.BlockingFifoList

See superclass/

clear() - Method in class org.jutil.java.collections.SynchronizedFifoList

See superclass/

clear() - Method in interface org.jutil.java.collections.Fifo

public behavior

post size() == 0;
Clear the list.

clear() - Method in class org.jutil.java.collections.BinomialHeap

See superclass

clear() - Method in class org.jutil.java.collections.Singleton

also public behavior

post false;
exception UnsupportedOperationException true;
See superclass

clear() - Method in class org.jutil.event.ChainNotifier

public behavior
assignable notifiers;
post notifiers.isEmpty();

clone() - Method in class org.jutil.math.matrix.Matrix

public behavior

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

clone() - Method in class org.jutil.math.matrix.Column

also public behavior

post \result instanceof Column;
See superclass

closure(Object) - Method in class org.jutil.java.collections.TransitiveClosure

// The given node may not be null.
pre startNode != null ;

post \result.equals(closureFromAll(new Singleton(o)));

signals (ConcurrentModificationException)
(* The collection was modified while calculating the tranitive closure.

closureFromAll(Set) - Method in class org.jutil.java.collections.TransitiveClosure

// The given set may not be null
pre startSet != null;
// The given set may not contain null references.
pre (\forall Object o ; startSet.contains(o) ; o != null);

// The result is effective.
post \result != null
// The transitive closure is the set of all nodes that can be reached from
// a start set of nodes via connections defined by
// public Set getConnectedNodes(Object node).
post isNaiveClosure(startSet, \result);
// Least Fixed Point
post (\forall Set cn;
(cn != null) && isNaiveClosure(startSet, cn);
(\result.size() <= cn.size()));
post_redundantly (\forall Object o; \result.contains(o); o != null);

signals (ConcurrentModificationException)
(* The collection was modified while calculating the tranitive closure.

CollectionOperator - interface org.jutil.java.collections.CollectionOperator.

CollectionOperator is the toplevel interface for collection operators.

Collections - class org.jutil.java.collections.Collections.

A utility class for perform operations on collections similar to java.util.Collections.

Collections() - Constructor for class org.jutil.java.collections.Collections

Column - class org.jutil.math.matrix.Column.

A class of matrices containing only 1 column.

Column(double[]) - Constructor for class org.jutil.math.matrix.Column

pre elements != 0
pre elements.length > 0

post size() == elements.length
post (\forall int i; i>0 && i <= size();
elementAt(i) == elements[i-1]);
Create a new Column with the given elements.

Column(int) - Constructor for class org.jutil.math.matrix.Column

public invariant getNbColumns() == 1;

pre size > 0;

post size() == size;
post (\forall int i; i > 0 && i <= size();
elementAt(i) == 0);
Create a new Column with the given size.

ComparableComparator - class org.jutil.java.collections.ComparableComparator.

Trivial Comparator that uses the Comparable interface of objects to compare.

ComparableComparator() - Constructor for class org.jutil.java.collections.ComparableComparator

compare(Object, Object) - Method in class org.jutil.java.collections.InverseComparator

public behavior

post \result == -getComparator().compare(first, second);
Return the inverse of the what the inverted comparator would return.

compare(Object, Object) - Method in class org.jutil.java.collections.ComparableComparator

public behavior

pre o1 instanceof Comparable;

post \result == ((Comparable)o1).compareTo(o2);
See superclass.

connectTo(StructureSet) - Method in class org.jutil.structure.StructureElement

public behavior

post getStructureSet() == set;
// If this StructureElement was connected before, and will now be
// connected to another StructureSet, it will be removed from the first one.
post \old(getStructureSet()) != null && \old(getStructureSet()) != set =>
! \old(getStructureSet()).contains(this);
post set != null ==> set.contains(this);
Set the 1 side of this 10n binding.

contains(ApplicabilityNotifier) - Method in class org.jutil.event.ChainNotifier

public behavior
post \result == notifiers.has(notifier);

contains(Object) - Method in class org.jutil.java.collections.SkipList

See superclass

contains(Object) - Method in class org.jutil.java.collections.Singleton

also public behavior

post \result ==
((getOnlyElement() == null) && (o == null)) ||
getOnlyElement().equals(o);
See superclass

contains(StructureElement) - Method in class org.jutil.structure.StructureSet

Check whether or not the given element is connected to this StructureSet.

containsExplicitly(Collection, Object) - Static method in class org.jutil.java.collections.Collections

public invariant_redundantly
(\forall Collection c; c != null;
(\forall Object o1; c.contains(o1);
(\exists Object o2; containsEplicitly(c, o2);
((o1 == null) && (o2 == null)) ||
((o1 != null) && (o1.equals(o2)))));

public invariant_redundantly
(\forall Collection c; c!= null;
(\forall Object o2; containsEplicitly(collection, o2);
c.contains(o2)));

public behavior

pre collection != null;

post \result == (\exists int i; i >= 0 && i < collection.toArray().length;
collection.toArray()[i] == element);
Check whether or not the given collection contains the given element when using == for comparison instead of equals().

copy(File, File) - Static method in class org.jutil.java.io.File

public behavior

pre source != null;
pre destination != null;
// both files must be different
pre ! source.getCanonicalPath().equals(destination.getCanonicalPath());

post (* The source file is copied to the destination file *);

signals (FileNotFoundException) (* The source file does not exist, is a directory
or not readable *);
signals (FileNotFoundException) (* The destination file does not exist and can not
be create, is a directory or exists, but is not
writable *);
signals (SecurityException) (* The source file may not be read from *);
signals (SecurityException) (* The destination file may not be writen to *);
signals (IOException) (* An IO errors occurs *);
Copies the given source file to the given destination file.

copyTo(File) - Method in class org.jutil.java.io.File

public behavior

pre destination != null;
// both files must be different
pre ! getCanonicalPath().equals(destination.getCanonicalPath());

post (* This file is copied to the destination file *);

signals (FileNotFoundException) (* This file does not exist, is a directory
or not readable *);
signals (FileNotFoundException) (* The destination file does not exist and can not
be create, is a directory or exists, but is not
writable *);
signals (SecurityException) (* This file may not be read from *);
signals (SecurityException) (* The destination file may not be writen to *);
signals (IOException) (* An IO errors occurs *);
Copies this file to the given destination file.

Counter - class org.jutil.java.collections.Counter.

An IntegerAccumulator that counts the number of items in a collection that satisfies some criterion.

Counter() - Constructor for class org.jutil.java.collections.Counter

criterion(Object) - Method in class org.jutil.java.collections.Filter

public behavior

pre isValidElement(element);

criterion(Object) - Method in class org.jutil.java.collections.ForAll

public behavior

pre isValidElement(element);

// criterion should be consistent with equals; subclass can say more
post (\forall object o1;;
(\forall object o2; o2.equals(o1); criterion(o1) == criterion(o2)));
Check whether the given object satisfies the criterion for this ForAll accumulator.

criterion(Object) - Method in class org.jutil.java.collections.Exists

also public behavior

post ! getCollection().contains(element) => \result == false;

public model boolean isValidElement(Object element);

public behavior

// criterion should be consistent with equals
post (\forall object o1;;
(\forall object o2;o2.equals(o1);criterion(o1) == criterion(o2)));

Check whether the given object satisfies the criterion for this Exists accumulator

criterion(Object) - Method in class org.jutil.java.collections.Counter

//As usual, criterion must be consistent with the semantics of equals
post (\forall Object o1;;
(\forall Object o2; o1.equals(o2);
criterion(o1) == criterion(o2)));
The criterion used to determine whether or not an element has to be counted.

criterion(Object) - Method in class org.jutil.java.collections.TypeFilter

also public behavior

// is of the desired type.
post \result == getType().isInstance(element);
See superclass

criterion(Object) - Method in class org.jutil.java.collections.AndFilter

also public behavior

post (\forall int i; i>=0 && i getFilters()[i].criterion(element));
See superclass

CVS_REVISION - Static variable in class org.jutil.java.collections.MapVisitor

CVS_REVISION - Static variable in class org.jutil.java.collections.TransitiveClosure

CVS_REVISION - Static variable in class org.jutil.java.collections.Filter

CVS_REVISION - Static variable in class org.jutil.java.collections.ObjectArrayIterator

CVS_REVISION - Static variable in class org.jutil.java.collections.Collections

CVS_REVISION - Static variable in interface org.jutil.java.collections.MapOperator

CVS_REVISION - Static variable in class org.jutil.java.collections.SkipListPQ

CVS_REVISION - Static variable in class org.jutil.java.collections.RobustVisitor

CVS_REVISION - Static variable in class org.jutil.java.collections.BooleanAccumulator

CVS_REVISION - Static variable in class org.jutil.java.collections.ForAll

CVS_REVISION - Static variable in class org.jutil.java.collections.Exists

CVS_REVISION - Static variable in class org.jutil.java.collections.Accumulator

CVS_REVISION - Static variable in class org.jutil.java.collections.RobustMapVisitor

CVS_REVISION - Static variable in class org.jutil.java.collections.IntegerAccumulator

CVS_REVISION - Static variable in class org.jutil.java.collections.Counter

CVS_REVISION - Static variable in class org.jutil.java.collections.Mapping

CVS_REVISION - Static variable in class org.jutil.java.collections.ZeroDimensionException

CVS_REVISION - Static variable in class org.jutil.java.collections.SkipList

CVS_REVISION - Static variable in class org.jutil.java.collections.Visitor

CVS_REVISION - Static variable in class org.jutil.java.collections.Arrays

CVS_REVISION - Static variable in class org.jutil.java.collections.TypeFilter

CVS_REVISION - Static variable in class org.jutil.java.collections.BinomialHeap

CVS_REVISION - Static variable in class org.jutil.java.collections.AndFilter

CVS_REVISION - Static variable in class org.jutil.java.collections.Singleton

CVS_REVISION - Static variable in class org.jutil.java.collections.ArrayCursor

CVS_REVISION - Static variable in interface org.jutil.java.collections.CollectionOperator

CVS_REVISION - Static variable in class org.jutil.java.reflect.Methods

CVS_REVISION - Static variable in class org.jutil.java.reflect.Classes

CVS_REVISION - Static variable in class org.jutil.java.throwable.StackTrace

CVS_REVISION - Static variable in class org.jutil.math.Math

CVS_REVISION - Static variable in class org.jutil.math.matrix.ExplicitShiftQRSchurDecomposer

CVS_REVISION - Static variable in class org.jutil.math.matrix.NMatrix

CVS_REVISION - Static variable in class org.jutil.math.matrix.Matrix

MvDMvDMvD : some operations don't have 2 sensible names for use as a mutator and inspector.

CVS_REVISION - Static variable in class org.jutil.math.matrix.Row

CVS_REVISION - Static variable in interface org.jutil.math.matrix.SchurDecomposition

CVS_REVISION - Static variable in interface org.jutil.math.matrix.QRDecomposer

CVS_REVISION - Static variable in class org.jutil.math.matrix.HouseholderQRDecomposition

CVS_REVISION - Static variable in class org.jutil.math.matrix.DefaultSchurDecomposition

CVS_REVISION - Static variable in interface org.jutil.math.matrix.EigenvalueDecomposition

CVS_REVISION - Static variable in interface org.jutil.math.matrix.SchurDecomposer

CVS_REVISION - Static variable in class org.jutil.math.matrix.QRLeastSquaresSolver

CVS_REVISION - Static variable in interface org.jutil.math.matrix.HessenbergReduction

CVS_REVISION - Static variable in class org.jutil.math.matrix.HouseholderHessenbergReduction

CVS_REVISION - Static variable in interface org.jutil.math.matrix.LinSolver

CVS_REVISION - Static variable in interface org.jutil.math.matrix.QRDecomposition

CVS_REVISION - Static variable in interface org.jutil.math.matrix.LUDecomposition

CVS_REVISION - Static variable in class org.jutil.math.matrix.PartialPivotGauss

CVS_REVISION - Static variable in interface org.jutil.math.matrix.CholeskyDecomposition

CVS_REVISION - Static variable in class org.jutil.math.matrix.HouseholderHessenbergReducer

CVS_REVISION - Static variable in class org.jutil.math.matrix.SchurEigenvalueDecomposer

CVS_REVISION - Static variable in class org.jutil.math.matrix.QRLinSolver

CVS_REVISION - Static variable in class org.jutil.math.matrix.SchurEigenvalueDecomposition

CVS_REVISION - Static variable in interface org.jutil.math.matrix.EigenvalueDecomposer

CVS_REVISION - Static variable in class org.jutil.math.matrix.LULinSolver

CVS_REVISION - Static variable in interface org.jutil.math.matrix.CholeskyDecomposer

CVS_REVISION - Static variable in class org.jutil.math.matrix.HouseholderQRDecomposer

CVS_REVISION - Static variable in interface org.jutil.math.matrix.HessenbergReducer

CVS_REVISION - Static variable in class org.jutil.math.matrix.Column

CVS_REVISION - Static variable in interface org.jutil.math.matrix.LeastSquaresSolver

CVS_REVISION - Static variable in class org.jutil.math.matrix.DefaultCholeskyDecomposition

CVS_REVISION - Static variable in class org.jutil.math.matrix.DefaultCholeskyDecomposer

CVS_REVISION - Static variable in interface org.jutil.math.matrix.LUDecomposer

CVS_REVISION - Static variable in class org.jutil.math.matrix.DefaultLUDecomposition

CVS_REVISION - Static variable in class org.jutil.junit.AbstractRevision

CVS_REVISION - Static variable in class org.jutil.junit.JutilTest

CVS_REVISION - Static variable in class org.jutil.junit.CVSRevision

CVS_REVISION - Static variable in class org.jutil.junit.RevisionError

CVS_REVISION - Static variable in interface org.jutil.junit.Revision

CVS_REVISION - Static variable in class org.jutil.structure.StructureElement

CVS_REVISION - Static variable in class org.jutil.structure.DoubleBinding

CVS_REVISION - Static variable in class org.jutil.structure.StructureSet

CVS_REVISION - Static variable in interface org.jutil.event.Notifier

CVS_REVISION - Static variable in class org.jutil.event.TypeApplicabilityNotifier

CVS_REVISION - Static variable in interface org.jutil.event.ApplicabilityNotifier

CVS_REVISION - Static variable in class org.jutil.event.ChainNotifier

CVS_REVISION - Static variable in class org.jutil.event.EventSourceSupport

CVSRevision - class org.jutil.junit.CVSRevision.

A class of CVS revisions.

CVSRevision(String) - Constructor for class org.jutil.junit.CVSRevision

public behavior

pre revision != null;
// The revision must either be a revision number, or a CVS revision string.
// In other words : "x.x.x.x" or "$Revision: 1.4 $".
pre new Pattern("\\d*(\\.(\\d)*)*").matcher(revision).matches() ||
new Pattern("$Revision: 1.4 $").matcher(revision).matches();

post (* number i == the i'th x *);
Initialize a new CVSRevision with the given String.

D

decompose(Matrix) - Method in class org.jutil.math.matrix.ExplicitShiftQRSchurDecomposer

See superclass

decompose(Matrix) - Method in interface org.jutil.math.matrix.QRDecomposer

public behavior

pre matrix != null;
pre matrix.getNbRows() >= matrix.getNbColumns();

post \result != null;
post (* \result.Q().times(\result.R()).equals(matrix) *);
post \result.R().getNbRows() == matrix.getNbRows();
post \result.R().getNbColumns() == matrix.getNbColumns();

decompose(Matrix) - Method in interface org.jutil.math.matrix.SchurDecomposer

public behavior

pre matrix != null;
pre matrix.isSquare();

post \result != null;
post (* \result.Q().times(\result.R()).equals(matrix) *);
post \result.Q().getNbRows() == matrix.getNbRows();

decompose(Matrix) - Method in class org.jutil.math.matrix.PartialPivotGauss

See superclass

decompose(Matrix) - Method in class org.jutil.math.matrix.SchurEigenvalueDecomposer

See superclass

decompose(Matrix) - Method in interface org.jutil.math.matrix.EigenvalueDecomposer

public behavior

pre matrix != null;
pre matrix.getNbRows() = matrix.getNbColumns();
pre (* matrix is not singular *);

post \result != null;
post (* \result.Q().times(\result.lambda()).equals(matrix) *);
post (* (\forall int i; i>=1 && i<= matrix.getNbRows();
\result.Q().times(\result.getEigenvector(i)).equals(\result.getEigenvector(i).times(\result.getEigenvalue(i))) *);
post \result.Q().getNbRows() == matrix.getNbRows();
post \result.Q().getNbColumns() == matrix.getNbColumns();

decompose(Matrix) - Method in interface org.jutil.math.matrix.CholeskyDecomposer

public behavior

pre matrix != null;
pre matrix.isSymmetric();
pre (* matrix is non-singular *);

post \result != null;
post (* \result.R().times(\result.R()).equals(matrix) *);

decompose(Matrix) - Method in class org.jutil.math.matrix.HouseholderQRDecomposer

The decomposition is done using the Householder algorithm.

decompose(Matrix) - Method in class org.jutil.math.matrix.DefaultCholeskyDecomposer

See superclass

decompose(Matrix) - Method in interface org.jutil.math.matrix.LUDecomposer

public behavior

pre matrix != null;
pre matrix.isSquare();

post \result != null;
post (* \result.L().times(\result.U()).equals(matrix) *);
post \result.L().getNbRows() == matrix.getNbRows();

DEFAULT - Static variable in class org.jutil.java.regex.Pattern

public invariant pattern() != null;

DefaultCholeskyDecomposer - class org.jutil.math.matrix.DefaultCholeskyDecomposer.

A class of objects that compute the Cholesky factorization of a symmetric matrix using the algorithm in the book of Trefethen and Bau.

DefaultCholeskyDecomposer() - Constructor for class org.jutil.math.matrix.DefaultCholeskyDecomposer

DefaultCholeskyDecomposition - class org.jutil.math.matrix.DefaultCholeskyDecomposition.

This class represents a Cholesky factorization of a matrix.

DefaultCholeskyDecomposition(Matrix) - Constructor for class org.jutil.math.matrix.DefaultCholeskyDecomposition

public behavior

pre R != null;
pre R.isUpperTriangular();
pre R.isSquare();

post R().equals(R);
Initialize a new DefaultCholeskyDecomposition with the given R matrix.

DefaultLUDecomposition - class org.jutil.math.matrix.DefaultLUDecomposition.

This class represents a default LU factorization of a square non-singular matrix.

DefaultLUDecomposition(Matrix, Matrix, Matrix) - Constructor for class org.jutil.math.matrix.DefaultLUDecomposition

public behavior

pre L != null;
pre L.isSquare();
pre L.isLowerTriangular();
pre (\forall int i; i>=1 && i<=L.getNbColumns();
L.elementAt(i,i) == 1);
pre U != null;
pre U.sameDimensions(L);
pre U.isUpperTriangular();
pre P != null;
pre P.isPermutationMatrix();
pre P.sameDimensions(L);

post L().equals(L);
post U().equals(U);
post P().equals(P);
Initialize a new DefaultLUDecomposition with the given L and U matrices

DefaultSchurDecomposition - class org.jutil.math.matrix.DefaultSchurDecomposition.

A class of schur decompositions of a matrix.

DefaultSchurDecomposition(Matrix, Matrix) - Constructor for class org.jutil.math.matrix.DefaultSchurDecomposition

public behavior

pre R != null;
pre R.isUpperTriangular;
pre Q != null;
pre Q.isUnary();

post R().equals(R);
post Q().equals(Q);
Initialize a new DefaultSchurDecomposition with the given R and Q matrices.

discard(Collection) - Method in class org.jutil.java.collections.Filter

public behavior

pre (\forall Object o, collection.contains(o); isValidElement(o));

// All elements that meet the criterion are removed from the collection
post collection != null ==> (\forall Object o; (o!= null) && (criterion(o)); ! \result.contains(o));
// is changed and returned.
post \result == collection;

signals (ConcurrentModificationException) (* The collection was modified while filtering *);

divide(double) - Method in class org.jutil.math.matrix.Matrix

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.

DOTALL - Static variable in class org.jutil.java.regex.Pattern

DoubleBinding - class org.jutil.structure.DoubleBinding.

A class of "components" for implementing a double binding.

DoubleBinding(DoubleBinding, Object) - Constructor for class org.jutil.structure.DoubleBinding

public behavior

pre object != null;

post getOtherBinding() == otherBinding;
post otherBinding != null ==> otherBinding.getOtherBinding == this;
// If was connected before to another object, that other object will
// be disconnected.
post (otherBinding != null) && \old(otherBinding.getOtherBinding()) != null ==>
\old(otherBinding.getOtherBinding()).getOtherBinding() == null;
post getObject() == object;
Initialize a new double binding connected to the given other DoubleBinding.

DoubleBinding(Object) - Constructor for class org.jutil.structure.DoubleBinding

public invariant getObject() != null;
public invariant getOtherBinding() != null =>
getOtherBinding().getOtherBinding() == this;

public behavior

pre object != null;

post getOtherBinding() == null;
post getObject() == object;
Initialize a new unconnected DoubleBinding.

E

EigenvalueDecomposer - interface org.jutil.math.matrix.EigenvalueDecomposer.

A class of objects that compute the eigenvalue factorization of a matrix.

EigenvalueDecomposition - interface org.jutil.math.matrix.EigenvalueDecomposition.

A class of eigenvalue decompositions of a matrix.

elementAt(int) - Method in class org.jutil.math.matrix.Row

pre validIndex(index);

post elementAt(1, index);
Return the element at the given index.

elementAt(int) - Method in class org.jutil.math.matrix.Column

pre validIndex(index);

post elementAt(index, 1);
Return the element at the given index

elementAt(int[]) - Method in class org.jutil.math.matrix.NMatrix

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

elementAt(int[]) - Method in class org.jutil.math.matrix.Matrix

elementAt(int, int) - Method in class org.jutil.math.matrix.Matrix

public behavior

pre validIndex(row, column);

post elementAt({row, column});
Return the element at the given row and column.

ensureExtended(Comparator) - Static method in class org.jutil.java.collections.ExtendedComparator

public behavior

pre comparator != null;

// The result must behave exactly the same as the given comparator.
post (\forall Object o1; ;
(\forall Object o2; ;
\result.compare(o1, o2) == comparator.compare(o1, o2)));
Ensure that the result is an ExtendedComparator.

equals(Object) - Method in class org.jutil.math.matrix.Matrix

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.

equals(Object) - Method in class org.jutil.junit.AbstractRevision

See superclass.

equals(Object) - Method in interface org.jutil.junit.Revision

public behavior

post (! (other instanceof Revision)) ==> (\result == false);
post (other instanceof Revision) ==> \result ==
(\forall int i; i>=1;
getNumber(i) == ((Revision)other).getNumber(i));
Check whether or not this revision is equal to another

EventSourceSupport - class org.jutil.event.EventSourceSupport.

This class is a support class for event sources.

EventSourceSupport() - Constructor for class org.jutil.event.EventSourceSupport

Exists - class org.jutil.java.collections.Exists.

A boolean exists operator.

Exists() - Constructor for class org.jutil.java.collections.Exists

ExplicitShiftQRSchurDecomposer - class org.jutil.math.matrix.ExplicitShiftQRSchurDecomposer.

A class of schur decomposers using an explict shift

ExplicitShiftQRSchurDecomposer(HessenbergReducer) - Constructor for class org.jutil.math.matrix.ExplicitShiftQRSchurDecomposer

public behavior

pre reducer != null;

post getHessenbergReducer() == reducer;
post getEpsilon ==
Initialize a new ExplicitShiftQRSchurDecomposer with the given HessenbergReducer

ExplicitShiftQRSchurDecomposer(HessenbergReducer, double) - Constructor for class org.jutil.math.matrix.ExplicitShiftQRSchurDecomposer

public behavior

pre reducer != null;
pre epsilon > 0;

post getHessenbergReducer() == reducer;
post getEpsilon() == epsilon;
Initialize a new ExplicitShiftQRSchurDecomposer with the given HessenbergReducer

ExtendedComparator - class org.jutil.java.collections.ExtendedComparator.

A Comparator with more convenient methods than java.util.Comparator.

ExtendedComparator() - Constructor for class org.jutil.java.collections.ExtendedComparator

F

Fifo - interface org.jutil.java.collections.Fifo.

Interface for first-in first-out like datastructures.

FifoList - class org.jutil.java.collections.FifoList.

FifoList is a class of objects that represent simple first-in first-out lists .

FifoList() - Constructor for class org.jutil.java.collections.FifoList

public behavior

post size() == 0;
Initialize a new empty FifoList.

File - class org.jutil.java.io.File.

A class that acts as an extension of java.io.File.

File(File, String) - Constructor for class org.jutil.java.io.File

Initialize a new File using the given parent and child.

File(String) - Constructor for class org.jutil.java.io.File

Initialize a new File See java.io.File.File(File, String).

File(String, String) - Constructor for class org.jutil.java.io.File

Initialize a new File See java.io.File.File(File, String).

Filter - class org.jutil.java.collections.Filter.

A filter for collections.

Filter() - Constructor for class org.jutil.java.collections.Filter

fireEvent(EventObject, Notifier) - Method in class org.jutil.event.EventSourceSupport

public behavior
pre notifier != null;
pre (\forall EventListener l; isValidListener(l);
notifier.isValidListener(l));
requires_redundantly (\forall EventListener l; listeners.has(l);
notifier.isValidListener(l));
pre notifier.isValidEvent(event);
assignable \fields_of(\reach(listeners)), \fields_of(\reach(event)),
\fields_of(\reach(notifier));
post (\forall EventListener l; listeners.has(l);
notifier.notifyEventListenerCalled(l, event));

flags() - Method in class org.jutil.java.regex.Pattern

Return the flags of this Pattern.

ForAll - class org.jutil.java.collections.ForAll.

A boolean for-all operator.

ForAll() - Constructor for class org.jutil.java.collections.ForAll

forwardSubstitute(Matrix, Column) - Method in class org.jutil.math.matrix.AbstractSolver

public behavior

pre L!= null;
pre b != null;
pre L.isSquare();
pre L.isLowerTriangular;
pre b.size() == L.getNbRows();
pre (* L is nonsingular *);

post (* L.times(\result).equals(b) *);

G

get(int) - Method in class org.jutil.event.ChainNotifier

public behavior
post \result == notifiers.itemAt(index);
signals (IndexOutOfBoundsException)
(index < 0) || (index >= notifiers.length());

getAllApplicableMethods(Class) - Static method in class org.jutil.java.reflect.Methods

// The given Class must be effective.
pre clazz != null;

// The result is Member
post \result instanceof Member;

getArray() - Method in class org.jutil.java.collections.ObjectArrayIterator

Return the array of this ObjectArrayIterator.

getArray() - Method in class org.jutil.java.collections.ZeroDimensionException

Return the array that caused this ZeroDimensionException.

getArrayDimensions(Object[]) - Static method in class org.jutil.java.collections.Arrays

// may not be null.
pre array != null;
Return the dimensions of the given array

getArrayType(Object) - Static method in class org.jutil.java.collections.Arrays

// may not be null.
pre array != null;
// must be an array.
pre array.getClass().isArray();
Return the type of an array

getColumn(int) - Method in class org.jutil.math.matrix.Matrix

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.

getComparator() - Method in class org.jutil.java.collections.InverseComparator

public behavior

post \result != null;
Return the comparator inverted by this.

getComparator() - Method in class org.jutil.java.collections.SkipListPQ

See superclass.

getComparator() - Method in class org.jutil.java.collections.SkipList

public behavior

post \result != null;
Return the Comparator used to determine the order in which the elements are added to this SkipList.

getComparator() - Method in interface org.jutil.java.collections.PriorityQueue

public behavior

post \result != null;
Return the comparator that is used to determine the order of the elements.

getComparator() - Method in class org.jutil.java.collections.BinomialHeap

See superclass.

getConnectedNodes(Object) - Method in class org.jutil.java.collections.TransitiveClosure

// The given node may not be null
pre node != null;

// Never returns null.
post \result != null;
// Never contains null.
post (\forall Object o; \result.contains(o); o != null);

getCursor() - Method in class org.jutil.java.collections.ArrayCursor

Return the index this ArrayCursor is pointing at.

getDecomposer() - Method in class org.jutil.math.matrix.QRLeastSquaresSolver

Return the QRDecomposer of this QRLeastSquaresSolver.

getDecomposer() - Method in class org.jutil.math.matrix.QRLinSolver

Return the QRDecomposer of this QRLinSolver.

getDecomposer() - Method in class org.jutil.math.matrix.LULinSolver

Return the LUDecomposer of this LULinSolver.

getDimensions() - Method in class org.jutil.java.collections.ArrayCursor

Return the dimensions of the array of this cursor.

getDimensions() - Method in class org.jutil.math.matrix.NMatrix

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

getDimensions() - Method in class org.jutil.math.matrix.Matrix

getEigenvalue(int) - Method in interface org.jutil.math.matrix.EigenvalueDecomposition

public behavior

pre index >= 1;
pre index <= getNbEigenvalues();

post \result == getEigenvalues().elementAt(index);
Return the index'th eigenvalue.

getEigenvalue(int) - Method in class org.jutil.math.matrix.SchurEigenvalueDecomposition

See superclass

getEigenvalues() - Method in interface org.jutil.math.matrix.EigenvalueDecomposition

public behavior

post \result != null;
post (\forall int i; i>=1 && i<=getNbEigenvalues();
\result.elementAt(i) != 0);
Return the eigenvalues.

getEigenvalues() - Method in class org.jutil.math.matrix.SchurEigenvalueDecomposition

See superclass

getEigenvector(int) - Method in interface org.jutil.math.matrix.EigenvalueDecomposition

public behavior

pre index >= 1;
pre index <= getNbEigenvalues();

post \result.equals(getEigenvectors.getColumn(index));
Return the index'th eigenvector.

getEigenvector(int) - Method in class org.jutil.math.matrix.SchurEigenvalueDecomposition

See superclass

getEigenvectors() - Method in interface org.jutil.math.matrix.EigenvalueDecomposition

public behavior

post \result != null;
Return the eigenvectors.

getEigenvectors() - Method in class org.jutil.math.matrix.SchurEigenvalueDecomposition

See superclass

getElement() - Method in class org.jutil.java.collections.ObjectArrayIterator

Return the element of the array at the current position of the iterator.

getEpsilon() - Method in class org.jutil.math.matrix.ExplicitShiftQRSchurDecomposer

public behavior

post \result > 0;
Return the precision with which the results must be computed.

getEventType() - Method in class org.jutil.event.TypeApplicabilityNotifier

public behavior
post \result == eventType;

getFilters() - Method in class org.jutil.java.collections.AndFilter

public behavior

post \result != null;
post (\forall int i; (i>=0) && (i Return the filters used by this AndFilter.

getFirst() - Method in class org.jutil.java.collections.SkipList

public behavior

pre ! isEmpty();

post contains(\result);
post (\forall Object o; contains(o);
getComparator().compare(\result,o)<=0);
Return the first object of this SkipList.

getHessenbergReducer() - Method in class org.jutil.math.matrix.ExplicitShiftQRSchurDecomposer

public behavior

post \result != null;
Return the HessenbergReducer used by this ExplicitShiftQRSchurDecomposer to calculate Schur decompositions.

getImmediateSuperTypes(Class) - Static method in class org.jutil.java.reflect.Classes

// The given Class must be effective
pre clazz != null;

// The set contains elements of type Class
post (\forall Object o; \result.contains(o); o instanceof Class);
// The set contains no null references
post (\forall Object o; \result.contains(o); o != null);
// The set only contains immediate supertypes of .
post (\forall Class c; \result.contains(c);
c == clazz.getSuperClass() || clazz.getInterfaces().contains(c));
// If the this method is applied to class Class, the result is the empty set.
post (clazz == Class.class) ==> \result.isEmpty();

getLinSolver() - Method in class org.jutil.math.matrix.SchurEigenvalueDecomposer

public behavior

post \result != null;
Return the LinSolver used by this SchurEigenvalueDecomposer to calculate eigenvalue decompositions.

getLinSolver() - Method in class org.jutil.math.matrix.SchurEigenvalueDecomposition

Return the LinSolver used to compute the eigenvectors.

getListenerType() - Method in class org.jutil.event.TypeApplicabilityNotifier

public behavior
post \result == listenerType;

getMajor() - Method in class org.jutil.junit.AbstractRevision

See superclass

getMajor() - Method in interface org.jutil.junit.Revision

public behavior

post \result == getNumber(1);
Return the major number of this Revision.

getMaxLevel() - Method in class org.jutil.java.collections.SkipList

public behavior

post \result >= 1;
Return the maximum level of this SkipList

getMicro() - Method in class org.jutil.junit.AbstractRevision

See superclass

getMicro() - Method in interface org.jutil.junit.Revision

public behavior

post \result == getNumber(3);
Return the micro number of this Revision.

getMinor() - Method in class org.jutil.junit.AbstractRevision

See superclass

getMinor() - Method in interface org.jutil.junit.Revision

public behavior

post \result == getNumber(2);
Return the minor number of this Revision.

getNbColumns() - Method in class org.jutil.math.matrix.Matrix

public behavior

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

getNbDimensions() - Method in class org.jutil.java.collections.ArrayCursor

// Returns the number of dimensions of the represented array.
post \result == getDimensions().length;
Return the number of dimensions of the array

getNbDimensions() - Method in class org.jutil.math.matrix.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.

getNbDimensions() - Method in class org.jutil.math.matrix.Matrix

getNbEigenvalues() - Method in interface org.jutil.math.matrix.EigenvalueDecomposition

public behavior

post \result > 0;
Return the number of eigenvalues.

getNbEigenvalues() - Method in class org.jutil.math.matrix.SchurEigenvalueDecomposition

See superclass

getNbRows() - Method in class org.jutil.math.matrix.Matrix

public behavior

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

getNotifiers() - Method in class org.jutil.event.ChainNotifier

public behavior
post isModelFor(notifiers, \result);

getNumber(int) - Method in class org.jutil.junit.CVSRevision

See superclass.

getNumber(int) - Method in interface org.jutil.junit.Revision

pre index >= 1;

post \result >=0;
post (index > length()) ==> (\result == 0);
Return the index'th number of this Revision.

getObject() - Method in class org.jutil.structure.StructureElement

public behavior

post \result != null;
Return the object on the n side of the 1-n binding represented by this StructureElement

getObject() - Method in class org.jutil.structure.DoubleBinding

Return the object at this side of the double binding.

getObject() - Method in class org.jutil.structure.StructureSet

Return the object at the 1 side of the 1-n binding.

getOnlyElement() - Method in class org.jutil.java.collections.Singleton

Return the only element in this Singleton.

getOtherBinding() - Method in class org.jutil.structure.DoubleBinding

Return the DoubleBinding object this one is connected to.

getOtherEnd() - Method in class org.jutil.structure.StructureElement

public behavior

post getStructureSet() == null => \result == null;
post getStructureSet() != null => \result == getStructureSet().getObject();
Return the Object at the other end of this double binding.

getOtherEnd() - Method in class org.jutil.structure.DoubleBinding

public behavior

post getOtherBinding() == null => \result == null;
post getOtherBinding() != null => \result == getOtherBinding().getObject();
Return the Object at the other end of this double binding.

getOtherEnds() - Method in class org.jutil.structure.StructureSet

public behavior

post (\forall Object o;;
\result.contains(o) <=>
(\exists StructureElement s; contains(s);
s.getObject().equals(o)));
post \result != null;
Return a set containing the objects at the n side of the 1-n binding.

getPattern() - Method in class org.jutil.java.regex.RegexReplacer

public behavior

post \result != null;
Return the pattern of this RegexReplacer.

getProbability() - Method in class org.jutil.java.collections.SkipList

public behavior

post \result >= 0;
post \result <= 1;
Return the probability that a node of level >= i is a node of level >= i + 1

getReplacement() - Method in class org.jutil.java.regex.RegexReplacer

public behavior

post \result != null;
Return the replacement string of this RegexReplacer.

getRow(int) - Method in class org.jutil.math.matrix.Matrix

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.

getSchurDecomposer() - Method in class org.jutil.math.matrix.SchurEigenvalueDecomposer

public behavior

post \result != null;
Return the SchurDecomposer used by this SchurEigenvalueDecomposer to calculate eigenvalue decompositions.

getSlider() - Method in class org.jutil.java.swing.SliderControlledLabel

Return the slider that controls the value of this SliderControlledLabel.

getStructureElements() - Method in class org.jutil.structure.StructureSet

public behavior

post (\forall StructuredElement s;;
contains(s) <=> \result.contains(s));
post \result != null;
Return a set containing the StructureElements at the n side of the 1-n binding.

getStructureSet() - Method in class org.jutil.structure.StructureElement

return the set this StructureElement belongs to

getSuperClasses(Class) - Static method in class org.jutil.java.reflect.Classes

// The given Class must be effective
pre clazz != null;

// The set contains elements of type Class
post (\forall Object o; \result.contains(o); o instanceof Class);
// The set contains no null references
post (\forall Class c; \result.contains(c); c != null);
// The set contains only classes, no interfaces.
post (\forall Class c; \result.contains(c); ! c.isInterface());
// The set contains only super classes of clazz.
post (\forall Class c; \result.contains(c); c.isAssignableFrom(clazz));
// The set contains all the super classes of .
post (\forall Class c; (c.isAssignableFrom(clazz)) && (! c.isInterface()); \result.contains(c));
// If is an interface, the set is empty.
post (clazz.isInterface()) ==> \result.size() == 0;

post (* The order of the result set is that subclasses are smaller
than superclasses.*);

getSuperTypes(Class) - Static method in class org.jutil.java.reflect.Classes

// The given Class must be effective
pre clazz != null;

// The set contains elements of type Class
post (\forall Object o; \result.contains(o); o instanceof Class);
// The set contains no null references
post (\forall Class c; \result.contains(c); c != null);
// The set contains only super types of clazz.
post (\forall Class c; \result.contains(c); c.isAssignableFrom(clazz));
// The set contains .
post \result.contains(clazz);
//If the this method is applied to class Object, the result
//is the singleton {Object}.
post (clazz == Object.class) ==> (\result.contains(Object.class)) &&
(\result.size() == 1);

getTestedClass() - Method in class org.jutil.junit.JutilTest

public behavior

post \result != null;
Return the class that is tested by this test class.

getTestedClassRevision() - Method in class org.jutil.junit.JutilTest

public behavior

post \result != null;
Return the field representing the revision of the tested class.

getTestedRevision() - Method in class org.jutil.junit.JutilTest

public behavior

post \result != null;
Return the revision of the tested class that is tested by this class.

getType() - Method in class org.jutil.java.collections.TypeFilter

public behavior

post \result != null;
Return the type of this TypeFilter.

getV(int) - Method in class org.jutil.math.matrix.HouseholderQRDecomposition

Return the i-th v vector as computed by the Householder algorithm that computed this QR decomposition.

getV(int) - Method in class org.jutil.math.matrix.HouseholderHessenbergReduction

public behavior

pre i>=1;
pre i<=H().getNbColumns() - 2;

post \result != null;

greater(Object, Object) - Method in class org.jutil.java.collections.ExtendedComparator

public behavior

post \result == (compare(first, second) > 0);

H

H() - Method in interface org.jutil.math.matrix.HessenbergReduction

public behavior

post \result != null;
post \result.isSquare();
post \result.isHessenberg();
Return the Hessenberg matrix of this HessenbergReduction.

H() - Method in class org.jutil.math.matrix.HouseholderHessenbergReduction

See superclass

hasNext() - Method in class org.jutil.java.collections.Singleton.SingletonIterator

also public behavior

post \result == onlyElementNotReturnedYet;
See superclass

HessenbergReducer - interface org.jutil.math.matrix.HessenbergReducer.

A class of matrix operators that compute the Hessenberg reduction of a matrix.

HessenbergReduction - interface org.jutil.math.matrix.HessenbergReduction.

A HessenbergReduction represents a Hessenberg reduction of a matrix.

HouseholderHessenbergReducer - class org.jutil.math.matrix.HouseholderHessenbergReducer.

A class of matrix operators that compute the Hessenberg reduction of a matrix using Householder reflections.

HouseholderHessenbergReducer() - Constructor for class org.jutil.math.matrix.HouseholderHessenbergReducer

HouseholderHessenbergReduction - class org.jutil.math.matrix.HouseholderHessenbergReduction.

This class represents a HouseHolder Hessenberg factorization of a matrix.

HouseholderHessenbergReduction(Matrix, Column[]) - Constructor for class org.jutil.math.matrix.HouseholderHessenbergReduction

public behavior

pre H != null;
pre H.isSquare();
pre H.isHessenberg();
pre vs != null;
pre vs.length == H.getNbColumns() - 2;
pre (\forall int i; i>=0 && i vs[i] != null
vs[i].size() == H.getNbRows() - i - 1);

post H().equals(H);
post (\forall int i; i>=1 && i<= vs.length;
getV(i).equals(vs[i-1]));
Initialize a new HouseholderHessenbergReduction combination with the given H matrix and v vectors.

HouseholderQRDecomposer - class org.jutil.math.matrix.HouseholderQRDecomposer.

A class of objects that compute the QR factorization of a matrix using the Householder Algorithm.

HouseholderQRDecomposer() - Constructor for class org.jutil.math.matrix.HouseholderQRDecomposer

HouseholderQRDecomposition - class org.jutil.math.matrix.HouseholderQRDecomposition.

This class represents a HouseHolder QR factorization of a matrix.

HouseholderQRDecomposition(Matrix, Column[]) - Constructor for class org.jutil.math.matrix.HouseholderQRDecomposition

public behavior

pre R != null;
pre R.isUpperTriangular();
pre vs != null;
pre vs.length == R.getNbRows();
pre (\forall int i; i>=0 && i vs[i] != null
vs[i].size() == R.getNbRows() - i);

post R().equals(R);
post (\forall int i; i>=1 && i<= vs.length;
getV(i).equals(vs[i-1]));
Initialize a new HouseholderQRDecomposition combination with the given R matrix and v vectors.

I

identical(Collection, Collection) - Static method in class org.jutil.java.collections.Collections

public behavior

// True if both collections are null
post ((first == null) && (second == null)) ==> \result == true;

// False if only one of both is null.
post ((first == null) || (second == null)) &&
!((first == null) && (second == null)) ==> \result ==false;

// If both collections are non-null, true if both collections
// have the same size and contains the exact same elements.
post ((first != null) && (second != null)) ==>
\result == (first.size() == second.size()) &&
(\forall Object o1; containsExplicitly(first, o1);
nbExplicitOccurrences(first,o1) == nbExplicitOccurrences(second, o2));
Check whether the two given collections contain the same elements.

identical(Map, Map) - Static method in class org.jutil.java.collections.Collections

// True if both maps are null
post ((first == null) && (second == null)) ==> \result == true;

// False if only one of both is null.
post ((first == null) || (second == null)) &&
!((first == null) && (second == null)) ==> \result ==false;

// If both maps are non-null, true if both maps
// have the same size and contains the same (key,value) pairs.
post ((first != null) && (second != null)) ==>
\result == (first.size() == second.size()) &&
(\forall Object k; first.containsKey(k);
second.containsKey(k) && second.get(k) == first.get(k)) &&
first.size() == second.size();
post (\forall Map.Entry e1; first.entrySet().contains(e1);
(\exists Map.Entry e2; second.entrySet().contains(e2);
(e1.getKey() == e2.getKey()) &&
Check whether the two given maps contain the same entries.

in(Collection) - Method in class org.jutil.java.collections.BooleanAccumulator

public behavior

pre (\forall Object o, collection.contains(o); isValidElement(o));

post (* the result of the accumulation is returned *);
post collection == null => \result == initialAccumulator();

signals (ConcurrentModificationException) (* The collection was modified while accumulating *);

in(Collection) - Method in class org.jutil.java.collections.ForAll

also public behavior

post \result == (\forall Object o; collection.contains(o); criterion(o));

in(Collection) - Method in class org.jutil.java.collections.Exists

also public behavior

post \result == (\exists Object o;collection.contains(o);criterion(o));

in(Collection) - Method in class org.jutil.java.collections.IntegerAccumulator

public behavior

pre (\forall Object o, collection.contains(o); isValidElement(o));

post (* the result of the accumulation is returned *);
post collection == null => \result == initialAccumulator();

signals (ConcurrentModificationException) (* The collection was modified while filtering *);

indexOf(ApplicabilityNotifier) - Method in class org.jutil.event.ChainNotifier

public behavior
post notifiers.has(notifier) ==>
\result == notifiers.indexOf(notifier);
post ! notifiers.has(notifier) ==> \result == -1;
ensures_redundantly \result >= -1;
Returns the index in this list of the first occurrence of the specified element, or -1 if this list does not contain this element.

initialAccumulator() - Method in class org.jutil.java.collections.BooleanAccumulator

Subclasses should implement this method to return the initialized accumulator.

initialAccumulator() - Method in class org.jutil.java.collections.ForAll

also public behavior

post \result == true;

initialAccumulator() - Method in class org.jutil.java.collections.Exists

also public behavior

// Returns false
post \result == false;

initialAccumulator() - Method in class org.jutil.java.collections.Accumulator

Subclasses should implement this method to return the initialized accumulator.

initialAccumulator() - Method in class org.jutil.java.collections.IntegerAccumulator

Subclasses should implement this method to return the initialized accumulator.

initialAccumulator() - Method in class org.jutil.java.collections.Counter

also public behavior

post \result == 0;

IntegerAccumulator - class org.jutil.java.collections.IntegerAccumulator.

An integer accumulator for collections.

IntegerAccumulator() - Constructor for class org.jutil.java.collections.IntegerAccumulator

InverseComparator - class org.jutil.java.collections.InverseComparator.

An ExtendedComparator that inverts another Comparator.

InverseComparator(Comparator) - Constructor for class org.jutil.java.collections.InverseComparator

public behavior

pre comparator != null;

post getComparator() == comparator;
Initialize a new InverseComparator with the given comparator.

isApplicable(EventListener, EventObject) - Method in class org.jutil.event.TypeApplicabilityNotifier

also
public behavior
pre listener != null;
post \result ==>
(listenerType.isInstance(listener) &&
((event == null) || eventType.isInstance(event)));
// remember that isInstance would be false when event == null

isApplicable(EventListener, EventObject) - Method in interface org.jutil.event.ApplicabilityNotifier

public behavior
pre listener != null;
post \result <== isValidListener(listener) && isValidEvent(event);

isConnected() - Method in class org.jutil.structure.DoubleBinding

Check whether or not this DoubleBinding is connected to another.

isDiagonal() - Method in class org.jutil.math.matrix.Matrix

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.

isEmpty() - Method in class org.jutil.java.collections.SkipListPQ

See superclass.

isEmpty() - Method in interface org.jutil.java.collections.PriorityQueue

public behavior

post \result == (size() == 0);
Check whether or not this PriorityQueue is empty.

isEmpty() - Method in class org.jutil.java.collections.FifoList

See superclass.

isEmpty() - Method in interface org.jutil.java.collections.Fifo

public behavior

post \result == (size() == 0);
Check whether or not this Fifo is empty.

isEmpty() - Method in class org.jutil.java.collections.BinomialHeap

See superclass.

isEmpty() - Method in class org.jutil.java.collections.Singleton

also public behavior

post \result == false;
See superclass

isEmpty() - Method in class org.jutil.event.ChainNotifier

public behavior
post \result == notifiers.isEmpty();

isEmpty() - Method in class org.jutil.event.EventSourceSupport

// The set of listeners.

isLowerTriangular() - Method in class org.jutil.math.matrix.Matrix

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

isNaiveClosure(Set, Set) - Method in class org.jutil.java.collections.TransitiveClosure

pre startSet != null
pre naiveClosureSet != null
post \result == (\forall Object o; startSet.contains(o);
(naiveClosureSet.contains(o) &&
(\exists Set ccn; isNaiveClosure(getConnectedNodes(o), ccn));
naiveClosureSet.containsAll(ccn)));
Transitive closure is a recursive definition.

isObjectArray(Class) - Static method in class org.jutil.java.collections.Arrays

// False is is null.
post (clazz == null) ==> (\result == false);
//Return true if is an array of objects.
post \result == clazz.isArray() &&
(clazz.getName().indexOf("[L") != -1);
Check whether the given class is an array of objects

isObjectArray(Object) - Static method in class org.jutil.java.collections.Arrays

// False is