org.jutil.event
Class EventSourceSupport

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

public class EventSourceSupport

extends java.lang.Object

This class is a support class for event sources. A source of events can delegate registration, deregistration and notification of listeners for a particular kind of event to an object of this class.

The actual source of the events should have delegation methods for all the add and removal method of this class with the correct static type for the Listener.

For adding and removing listeners to the set, equals() is used.

isValidEvent(EventListener) is used as an abstract type invariant and as an abstract precondition in add(EventListener). This makes it possible to transport information about the listeners available in subtypes, thru add(EventListener) and fireEvent(EventObject, Notifier) to the Notifier that will take care of the actual dispatch of an event to a listener.

Version:

$Revision: 1.3 $

Author:

Jan Dockx, Marko van Dooren

Field Summary

static java.lang.String

CVS_REVISION

Constructor Summary

EventSourceSupport()

Method Summary

void	add(java.util.EventListener listener) public behavior pre listener != null ==> isValidListener(listener); assignable listeners; // The given Listener is now in the set of listeners, if it is not null. post listener != null ==> listeners.equals(\old(listeners.insert(listener))); ensures_redundantly listener != null ==> listeners.has(listener); Add an event Listener to the listeners to be notified by this.
void	fireEvent(java.util.EventObject event, Notifier notifier) public behavior pre notifier != null; pre (\forall EventListener l; isValidListener(l); notifier.isValidListener(l)); requires_redundantly (\forall EventListener l; listeners.has(l); notifier.isValidListener(l)); pre notifier.isValidEvent(event); assignable \fields_of(\reach(listeners)), \fields_of(\reach(event)), \fields_of(\reach(notifier)); post (\forall EventListener l; listeners.has(l); notifier.notifyEventListenerCalled(l, event));
boolean	isEmpty() // The set of listeners.
void	remove(java.util.EventListener listener) public behavior assignable listeners; // The given listener is not in the set of listeners. post listeners.equals(\old(listeners.remove(listener))); ensures_redundantly ! listeners.has(listener); Remove an event EventListener from the listeners to be notified by this.
java.lang.String	toString() A String representation of this.

Methods inherited from class java.lang.Object

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

Field Detail

CVS_REVISION

public static final java.lang.String CVS_REVISION

Constructor Detail

EventSourceSupport

public EventSourceSupport()

Method Detail

isEmpty

public final boolean isEmpty()

// The set of listeners. Because it is a set, it does contain duplicates.
public model JMLObjectSet listeners
initially listeners != null && listeners.isEmpty();
// The set of listeners is never null.
public invariant listeners != null;
// The set of listeners contains no null references.
public invariant ! listeners.has(null);
// The listeners are all EventListeners.
public invariant (\forall Object o; listeners.has(o);
o instanceof EventListener);
// The listeners are all valid.
public invariant (\forall EventListener l; listeners.has(l);
isValidListener(l));

public behavior
post \result <==> listeners.isEmpty();

add

public final void add(java.util.EventListener listener)

public behavior
pre listener != null ==> isValidListener(listener);
assignable listeners;
// The given Listener is now in the set of listeners, if it is not null.
post listener != null ==> listeners.equals(\old(listeners.insert(listener)));
ensures_redundantly listener != null ==> listeners.has(listener);
Add an event Listener to the listeners to be notified by this. If the listener is already registered, the method has reached its goal without doing anything.

Parameters:

listener - The Listener which is to be added to the list of listeners.

remove

public final void remove(java.util.EventListener listener)

public behavior
assignable listeners;
// The given listener is not in the set of listeners.
post listeners.equals(\old(listeners.remove(listener)));
ensures_redundantly ! listeners.has(listener);
Remove an event EventListener from the listeners to be notified by this.

Parameters:

listener - The EventListener which is to be removed from the list of listeners.

fireEvent

public final void fireEvent(java.util.EventObject event,
                            Notifier notifier)

public behavior
pre notifier != null;
pre (\forall EventListener l; isValidListener(l);
notifier.isValidListener(l));
requires_redundantly (\forall EventListener l; listeners.has(l);
notifier.isValidListener(l));
pre notifier.isValidEvent(event);
assignable \fields_of(\reach(listeners)), \fields_of(\reach(event)),
\fields_of(\reach(notifier));
post (\forall EventListener l; listeners.has(l);
notifier.notifyEventListenerCalled(l, event));

Calls #notifyEventListener(EventListener, EventObject) on all listeners with the given event.

The model inspector {#isValidListener(EventListener)} can be used to transport information about the registered listeners, thru this method, to the actual dispatch method in notifier.

Parameters:

event - The event to be sent to all registered listeners.

notifier - The notifier that will dispatch the event to the registered listeners.

toString

public java.lang.String toString()

A String representation of this. Lists all currently registered listeners.

Overrides:

toString in class java.lang.Object