org.jutil.java.collections
Class ArrayCursor

java.lang.Object
  |
  +--org.jutil.java.collections.ArrayCursor

public class ArrayCursor

extends java.lang.Object

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

Version:

$Revision: 1.6 $

Author:

Marko van Dooren

Field Summary

static java.lang.String

CVS_REVISION

Constructor Summary

ArrayCursor(java.lang.Object[] theArray)
// 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.

Method Summary

boolean	atEnd() // 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.
boolean	atStart() // 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.
int[]	getCursor() Return the index this ArrayCursor is pointing at.
int[]	getDimensions() Return the dimensions of the array of this cursor.
int	getNbDimensions() // Returns the number of dimensions of the represented array. post \result == getDimensions().length; Return the number of dimensions of the array
void	next() // The cursor is set to the next element. Set this cursor to the next element in the array.
void	previous() // The cursor is set to the previous element. Set this cursor to the previous element in the array.
void	toEnd() // The iterator will be positioned at the end of the array. post atEnd()==true; Set this ArrayCursor to the end of the array.
void	toStart() // The iterator will be positioned at the beginning of the array. post atStart()==true; Set this ArrayCursor to the beginning of the array.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

CVS_REVISION

public static final java.lang.String CVS_REVISION

Constructor Detail

ArrayCursor

public ArrayCursor(java.lang.Object[] theArray)
            throws ZeroDimensionException

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

Method Detail

getNbDimensions

public int getNbDimensions()

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

getDimensions

public int[] getDimensions()

Return the dimensions of the array of this cursor.

getCursor

public int[] getCursor()

Return the index this ArrayCursor is pointing at.

atStart

public boolean atStart()

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

atEnd

public boolean atEnd()

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

next

public void next()
          throws java.util.NoSuchElementException

// The cursor is set to the next element.
Set this cursor to the next element in the array.

previous

public void previous()
              throws java.util.NoSuchElementException

// The cursor is set to the previous element.
Set this cursor to the previous element in the array.

toStart

public void toStart()

// The iterator will be positioned at the beginning of the array.
post atStart()==true;
Set this ArrayCursor to the beginning of the array.

toEnd

public void toEnd()

// The iterator will be positioned at the end of the array.
post atEnd()==true;
Set this ArrayCursor to the end of the array.