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.

Class Specifications

public invariant getDimensions() != null; public invariant ( \forall int i; i >= 0&&i < getDimensions().length; getDimensions()[i] > 0); public invariant getDimensions().equals(Arrays.getArrayDimensions(array)); public invariant getCursor() != null; public invariant getCursor().length == getDimensions().length; public invariant ( \forall int i; i >= 0&&i < getCursor().length; (getCursor()[i] >= 0)&&(getCursor()[i] < getDimensions()[i]));

Model Field Summary
java.lang.Object[]	array

 

Field Summary
static java.lang.String	CVS_REVISION

 

Constructor Summary

ArrayCursor(java.lang.Object[] theArray)           Initialize a new ArrayCursor for a given array of objects.

 

Method Summary
boolean	atEnd()           Check whether this cursor points to the end of the array.
boolean	atStart()           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()           Return the number of dimensions of the array
void	next()           Set this cursor to the next element in the array.
void	previous()           Set this cursor to the previous element in the array.
void	toEnd()           Set this ArrayCursor to the end of the array.
void	toStart()           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

 

Model Field Detail

array

public java.lang.Object[] array

CVS_REVISION

public static final java.lang.String CVS_REVISION

ArrayCursor

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

Initialize a new ArrayCursor for a given array of objects.

Specifications:

requires array != null;
ensures getDimensions().equals(Arrays.getArrayDimensions(theArray));
ensures array == theArray;

getNbDimensions

public int getNbDimensions()

Return the number of dimensions of the array

Specifications:

ensures \result == getDimensions().length;

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

Check whether this cursor points to the beginning of the array.

Specifications:

ensures \result == ( \forall int i; i >= 0&&i < getCursor().length; getCursor()[i] == 0);

atEnd

public boolean atEnd()

Check whether this cursor points to the end of the array.

Specifications:

ensures \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);

next

public void next()
          throws java.util.NoSuchElementException

Set this cursor to the next element in the array.

previous

public void previous()
              throws java.util.NoSuchElementException

Set this cursor to the previous element in the array.

toStart

public void toStart()

Set this ArrayCursor to the beginning of the array.

Specifications:

ensures atStart() == true;

toEnd

public void toEnd()

Set this ArrayCursor to the end of the array.

Specifications:

ensures atEnd() == true;