Overview  Package   Class  Tree  Deprecated  Index  Help 
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES
SUMMARY:  INNER | FIELD | CONSTR | METHOD DETAIL:  FIELD | CONSTR | METHOD

org.jutil.event
Class ChainNotifier

java.lang.Object
  |
  +--org.jutil.event.ChainNotifier
All Implemented Interfaces:
ListenerValidity, Notifier
public final class ChainNotifier
extends java.lang.Object
implements Notifier

Class Specifications
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);
depends notifiers <- \fields_of($chainElements);
represents notifiers \such_that isModelFor(notifiers,$chainElements);

Model Field Summary
 org.jmlspecs.models.JMLObjectSequence notifiers
           
 
Field Summary
static java.lang.String CVS_REVISION
           
 
Constructor Summary
ChainNotifier()
           
 
Method Summary
 void add(int index, ApplicabilityNotifier notifier)
          Inserts the specified element at the specified position in this list.
 void add(ApplicabilityNotifier notifier)
          Appends the specified element to the end of this list.
 void clear()
           
 boolean contains(ApplicabilityNotifier notifier)
           
 java.lang.Object get(int index)
           
 java.util.List getNotifiers()
           
 int indexOf(ApplicabilityNotifier notifier)
          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()
           
static boolean isModelFor(org.jmlspecs.models.JMLObjectSequence jmlSeq, java.util.List javaList)
          jmlSeq and javaList contain the same elements in the same order.
 int lastIndexOf(ApplicabilityNotifier notifier)
          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)
          Subclasses need to overwrite this method to call the call-back method defined in listenerType with event. The postcondition is abstract.
 ApplicabilityNotifier remove(int index)
           
 void remove(ApplicabilityNotifier notifier)
           
 ApplicabilityNotifier set(int index, ApplicabilityNotifier notifier)
          Replaces the element at the specified position in this list with the specified element.
 int size()
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 
Methods inherited from interface org.jutil.event.Notifier
isValidEvent, notifyEventListenerCalled
 
Methods inherited from interface org.jutil.event.ListenerValidity
isValidListener
 

Model Field Detail

notifiers

public org.jmlspecs.models.JMLObjectSequence notifiers
Field Detail

CVS_REVISION

public static final java.lang.String CVS_REVISION
Constructor Detail

ChainNotifier

public ChainNotifier()
Specifications:
public behavior
assignable notifiers;
ensures notifiers.isEmpty();
Method Detail

notifyEventListener

public void notifyEventListener(java.util.EventListener listener,
                                java.util.EventObject event)
Description copied from interface: Notifier

Subclasses need to overwrite this method to call the call-back method defined in listenerType with event.

The postcondition is abstract. This is used in EventSourceSupport to specify that this method will indeed be called by EventSourceSupport.fireEvent(EventObject, Notifier).

Specifications inherited from overridden method in interface Notifier:
public behavior
requires listener != null;
requires isValidListener(listener);
requires isValidEvent(event);
assignable \fields_of(\reach(listener)), \fields_of(\reach(event)), \fields_of(\reach(this));
ensures notifyEventListenerCalled(listener,event);

size

public final int size()
Specifications: pure
public behavior
ensures \result == notifiers.length();

isEmpty

public final boolean isEmpty()
Specifications: pure
public behavior
ensures \result == notifiers.isEmpty();

contains

public final boolean contains(ApplicabilityNotifier notifier)
Specifications: pure
public behavior
ensures \result == notifiers.has(notifier);

remove

public final void remove(ApplicabilityNotifier notifier)
Specifications:
public behavior
assignable notifiers;
ensures notifiers.equals(\old(notifiers.removeItemAt(notifiers.indexOf(notifier))));

add

public final void add(ApplicabilityNotifier notifier)
Appends the specified element to the end of this list.

Specifications:
public behavior
assignable notifiers if notifier != null;
ensures notifier != null ==> notifiers.equals(\old(notifiers.insertBack(notifier)));

clear

public final void clear()
Specifications:
public behavior
assignable notifiers;
ensures notifiers.isEmpty();

get

public final java.lang.Object get(int index)
                           throws java.lang.IndexOutOfBoundsException
Specifications: pure
public behavior
ensures \result == notifiers.itemAt(index);
signals (IndexOutOfBoundsException) (index < 0)||(index >= notifiers.length());

set

public final ApplicabilityNotifier set(int index,
                                       ApplicabilityNotifier notifier)
                                throws java.lang.IndexOutOfBoundsException
Replaces the element at the specified position in this list with the specified element.

Specifications:
public behavior
assignable notifiers if notifier != null;
ensures notifier != null ==> notifiers.equals(\old(notifiers.replaceItemAt(index,notifier)));
ensures notifier != null ==> \result == \old(notifiers.itemAt(index));
ensures notifier == null ==> \result == null;
signals (IndexOutOfBoundsException) (index < 0)||(index >= notifiers.length());

add

public void add(int index,
                ApplicabilityNotifier notifier)
         throws java.lang.IndexOutOfBoundsException
Inserts the specified element at the specified position in this list.

Specifications:
public behavior
assignable notifiers if notifier != null;
ensures notifier != null ==> notifiers.equals(\old(notifiers.insertBeforeIndex(index,notifier)));
signals (IndexOutOfBoundsException) (index < 0)||(index >= notifiers.length());

remove

public ApplicabilityNotifier remove(int index)
                             throws java.lang.IndexOutOfBoundsException
Specifications:
public behavior
assignable notifiers;
ensures notifiers.equals(\old(notifiers.removeItemAt(index)));
signals (IndexOutOfBoundsException) (index < 0)||(index >= notifiers.length());

indexOf

public int indexOf(ApplicabilityNotifier notifier)
Returns the index in this list of the first occurrence of the specified element, or -1 if this list does not contain this element.

Specifications: pure
public behavior
ensures notifiers.has(notifier) ==> \result == notifiers.indexOf(notifier);
ensures !notifiers.has(notifier) ==> \result == -1;
ensures_redundantly \result >= -1;

lastIndexOf

public int lastIndexOf(ApplicabilityNotifier notifier)
Returns the index in this list of the last occurrence of the specified element, or -1 if this list does not contain this element.

Specifications:
public behavior
ensures notifiers.has(notifier) ==> \result == notifiers.length()-notifiers.reverse().indexOf(notifier);
ensures !notifiers.has(notifier) ==> \result == -1;
ensures_redundantly \result >= -1;

getNotifiers

public java.util.List getNotifiers()
Specifications: pure
public behavior
ensures isModelFor(notifiers,\result );

isModelFor

public static boolean isModelFor(org.jmlspecs.models.JMLObjectSequence jmlSeq,
                                 java.util.List javaList)
jmlSeq and javaList contain the same elements in the same order.

Specifications:
public behavior
requires jmlSeq != null;
requires javaList != null;
ensures \result <==> (jmlSeq.length() == javaList.size())&&( \forall int i; 0 <= i&&i < jmlSeq.length(); jmlSeq.itemAt(i) == javaList.get(i));
Overview  Package   Class  Tree  Deprecated  Index  Help 
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES
SUMMARY:  INNER | FIELD | CONSTR | METHOD DETAIL:  FIELD | CONSTR | METHOD