org.jutil.event
Class ChainNotifier

java.lang.Object
  |
  +--org.jutil.event.ChainNotifier

All Implemented Interfaces:

Notifier

public final class ChainNotifier

extends java.lang.Object

implements Notifier

Version:

$Revision: 1.3 $

Author:

Jan Dockx

Field Summary

static java.lang.String

CVS_REVISION

Constructor Summary

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

Method Summary

void	add(ApplicabilityNotifier notifier) 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.
void	add(int index, ApplicabilityNotifier notifier) 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.
void	clear() public behavior assignable notifiers; post notifiers.isEmpty();
boolean	contains(ApplicabilityNotifier notifier) public behavior post \result == notifiers.has(notifier);
java.lang.Object	get(int index) public behavior post \result == notifiers.itemAt(index); signals (IndexOutOfBoundsException) (index < 0) || (index >= notifiers.length());
java.util.List	getNotifiers() public behavior post isModelFor(notifiers, \result);
int	indexOf(ApplicabilityNotifier notifier) 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.
boolean	isEmpty() public behavior post \result == notifiers.isEmpty();
int	lastIndexOf(ApplicabilityNotifier notifier) public behavior post notifiers.has(notifier) ==> \result == notifiers.length() - notifiers.reverse().indexOf(notifier); post ! notifiers.has(notifier) ==> \result == -1; ensures_redundantly \result >= -1; Returns the index in this list of the last occurrence of the specified element, or -1 if this list does not contain this element.
void	notifyEventListener(java.util.EventListener listener, java.util.EventObject event) public invariant notifiers != null; public invariant (\forall Object o; notifiers.has(o); o != null); public invariant (\forall Object o; notifiers.has(o); o instanceof ApplicabilityNotifier); public model JMLObjectSequence notifiers;
void	remove(ApplicabilityNotifier notifier) public behavior assignable notifiers; post notifiers.equals(\old(notifiers.removeItemAt( notifiers.indexOf(notifier))));
ApplicabilityNotifier	remove(int index) public behavior assignable notifiers; post notifiers.equals(\old(notifiers.removeItemAt(index))); signals (IndexOutOfBoundsException) (index < 0) || (index >= notifiers.length());
ApplicabilityNotifier	set(int index, ApplicabilityNotifier notifier) public behavior assignable notifiers if notifier != null; post notifier != null ==> notifiers.equals(\old(notifiers.replaceItemAt(index, notifier))); post notifier != null ==> \result == \old(notifiers.itemAt(index)); post notifier == null ==> \result == null; signals (IndexOutOfBoundsException) (index < 0) || (index >= notifiers.length()); Replaces the element at the specified position in this list with the specified element.
int	size() public behavior post \result == notifiers.length();

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

ChainNotifier

public ChainNotifier()

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

Method Detail

notifyEventListener

public void notifyEventListener(java.util.EventListener listener,
                                java.util.EventObject event)

public invariant notifiers != null;
public invariant (\forall Object o; notifiers.has(o); o != null);
public invariant (\forall Object o; notifiers.has(o);
o instanceof ApplicabilityNotifier);

public model JMLObjectSequence notifiers;

Specified by:

notifyEventListener in interface Notifier

size

public final int size()

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

isEmpty

public final boolean isEmpty()

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

contains

public final boolean contains(ApplicabilityNotifier notifier)

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

remove

public final void remove(ApplicabilityNotifier notifier)

public behavior
assignable notifiers;
post notifiers.equals(\old(notifiers.removeItemAt(
notifiers.indexOf(notifier))));

add

public final void add(ApplicabilityNotifier notifier)

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.

clear

public final void clear()

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

get

public final java.lang.Object get(int index)
                           throws java.lang.IndexOutOfBoundsException

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

set

public final ApplicabilityNotifier set(int index,
                                       ApplicabilityNotifier notifier)
                                throws java.lang.IndexOutOfBoundsException

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

add

public void add(int index,
                ApplicabilityNotifier notifier)
         throws java.lang.IndexOutOfBoundsException

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.

remove

public ApplicabilityNotifier remove(int index)
                             throws java.lang.IndexOutOfBoundsException

public behavior
assignable notifiers;
post notifiers.equals(\old(notifiers.removeItemAt(index)));
signals (IndexOutOfBoundsException)
(index < 0) || (index >= notifiers.length());

indexOf

public int indexOf(ApplicabilityNotifier notifier)

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.

lastIndexOf

public int lastIndexOf(ApplicabilityNotifier notifier)

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

getNotifiers

public java.util.List getNotifiers()

public behavior
post isModelFor(notifiers, \result);