com.eliad.util
Interface Intervals

All Known Subinterfaces:

RulerModel

All Known Implementing Classes:

SizeSequenceIntervals

public interface Intervals

extends java.io.Serializable, java.lang.Cloneable

A basic SizeSequence functionality in the form of an interface. This object can answer queries about the size and positions of the items.

Since this is meant to be a low-level interface, we do not make it a source of events. Yet it is a model, albeit a simple one, and notifications about change may be needed. For instance, a caching proxy would need to be aware of the modifications, and it would be difficult to guarantee that the model would only be accessed through the proxy.

Invariants:

getCount() >= 0

forall int i in [0, getCount() [ | getSize(i) >= 0

getPosition(0) == 0

forall int i in [1, getCount()+1 [ | getPosition(i) >= 0

forall int i in [0, getCount() [ | getSize(i) == getPosition(i+1) - getPosition(i)

forall int i in [0, getCount() [ | forall int j in [i+1, getCount() [ | getSize(i) != getSize(j) implies !hasFixedSize()

hasFixedSize() implies forall i in [0, getCount() [ | getSize(i) == getDefaultSize()

forall int x <0 | getIndex(x) == -1

getIndex(0) == 0

forall int x >=0 | getIndex(x) <= getCount()

forall int x >=0 | forall int y > x | getIndex(x) <= getIndex(y)

forall int i in [0, getCount() [ | getIndex(getPosition(i)) == i

Version:

1.0 00/03/26

Author:

Patrick Mérissert-Coffinières

Inner Class Summary

static class

Intervals.Factory A factory to clone Interval objects and create default ones.

Method Summary

java.lang.Object	clone() Necessary to allow public access to the clone method.
int	getCount() Returns the number of entries in this Intervals object
int	getDefaultSize() returns the default size for new entries
int	getIndex(int position) Returns the index of the entry that contains the specified position.
int	getPosition(int index) Returns the start position for the specified entry.
int	getSize(int index) Returns the size of the specified entry.
int[]	getSizes() Returns the array of sizes for all entries.
boolean	hasFixedSize() Tests whether all the entries are the same size
void	insertEntries(int start, int length, int value) Adds a continuous group of entries to this Intervals.
void	removeEntries(int start, int length) Removes a continuous group of entries from this Intervals.
void	setFixedSize(int size) Sets a common size for all entries.
void	setSize(int index, int size) Sets the size of the specified entry.
void	setSizes(int[] sizes) Sets the sizes for all entries from an array

Method Detail

getDefaultSize

public int getDefaultSize()

returns the default size for new entries

getCount

public int getCount()

Returns the number of entries in this Intervals object

Returns:

the number of entries

Postconditions:

return >= 0

getSize

public int getSize(int index)

Returns the size of the specified entry.

Parameters:

index - the index corresponding to the entry

Returns:

the size of the entry

Preconditions:

index >= 0 && index < getCount()

Postconditions:

return >= 0

return == getPosition(index+1) - getPosition(x)

setSize

public void setSize(int index,
                    int size)

Sets the size of the specified entry.

Parameters:

index - the index corresponding to the entry

size - the size of the entry

Preconditions:

index >= 0 && index < getCount()

size > 0

Postconditions:

getSize(index) == size

forall i in [0, getCount()[ | i != index implies getSize(i) == getSize(i)@pre

setFixedSize

public void setFixedSize(int size)

Sets a common size for all entries. This becomes the new default size.

Parameters:

size - the size of the entries

Preconditions:

size >= 0

Postconditions:

hasFixedSize() && getDefaultSize() == size

hasFixedSize

public boolean hasFixedSize()

Tests whether all the entries are the same size

getIndex

public int getIndex(int position)

Returns the index of the entry that contains the specified position.

Parameters:

position - the position of the entry

Returns:

the index of the entry that occupies the specified position

Postconditions:

position >=0 && position < getPosition(getCount()) implies return >= 0 && return < getCount()

position <0 implies return == -1

position >= getPosition(getCount()) implies return == getCount()

getPosition

public int getPosition(int index)

Returns the start position for the specified entry.

Parameters:

index - the index of the entry with the desired position.

Returns:

the starting position of the specified entry. Note that it may be one higher than the argument to getSize(int).

Preconditions:

index >= 0 && index <= getCount()

Postconditions:

return >= 0

index==0 implies return ==0

getIndex(return) == return

getSizes

public int[] getSizes()

Returns the array of sizes for all entries.

Postconditions:

return.length == getCount()

index >= 0 && index < getCount() implies return[index] >= 0

setSizes

public void setSizes(int[] sizes)

Sets the sizes for all entries from an array

Postconditions:

index >= 0 && index < sizes.length implies sizes[index] >= 0

getCount() == sizes.count

insertEntries

public void insertEntries(int start,
                          int length,
                          int value)

Adds a continuous group of entries to this Intervals.

Parameters:

start - the index to be assigned to the first entry in the group

length - the number of entries in the group

value - the size to be assigned to each new entry

Preconditions:

start >= 0

length > 0

Postconditions:

getCount() == getCount()@pre + length

removeEntries

public void removeEntries(int start,
                          int length)

Removes a continuous group of entries from this Intervals.

Parameters:

start - the index of the first entry to be removed

length - the number of entries to be removed

Preconditions:

start >= 0

length > 0

Postconditions:

start+length <= getCount()@pre implies getCount() == getCount()@pre - length

clone

public java.lang.Object clone()
                       throws java.lang.CloneNotSupportedException

Necessary to allow public access to the clone method.

Overrides:

clone in class java.lang.Object