org.jutil.event
Class EventSourceSupport

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

All Implemented Interfaces:

ListenerValidity

public class EventSourceSupport

extends java.lang.Object

implements ListenerValidity

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.

Class Specifications

public invariant listeners != null; public invariant !listeners.has(null); public invariant ( \forall Object o; listeners.has(o); o instanceof EventListener); public invariant ( \forall EventListener l; listeners.has(l); isValidListener(l));

Model Field Summary
org.jmlspecs.models.JMLObjectSet	listeners

 

Field Summary
static java.lang.String	CVS_REVISION

 

Constructor Summary

EventSourceSupport()

 

Method Summary
void	add(java.util.EventListener listener)           Add an event Listener to the listeners to be notified by this.
void	fireEvent(java.util.EventObject event, Notifier notifier)           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.
boolean	isEmpty()
static boolean	isModelFor(org.jmlspecs.models.JMLObjectSet jmlSet, java.util.Set javaSet)           jmlSet and javaSet contain the same elements.
boolean	isValidListener(java.util.EventListener listener)           This model inspector can be used as an abstract precondition in methods using EventLister arguments, limiting which instances are acceptable. It can be used to transport information about listeners from the type invariants to the implementation of the method that uses it as a precondition. // JDJDJD // Adding listener != null here would result in \result <== listener != null;, // because the postcondition needs to be open for strengthening in subtypes.
void	remove(java.util.EventListener 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

 

Model Field Detail

listeners

public org.jmlspecs.models.JMLObjectSet listeners

Specifications:
     initially listeners != null&&listeners.isEmpty()

CVS_REVISION

public static final java.lang.String CVS_REVISION

EventSourceSupport

public EventSourceSupport()

isValidListener

public boolean isValidListener(java.util.EventListener listener)

Description copied from interface: ListenerValidity

This model inspector can be used as an abstract precondition in methods using EventLister arguments, limiting which instances are acceptable.

It can be used to transport information about listeners from the type invariants to the implementation of the method that uses it as a precondition.

// JDJDJD // Adding listener != null here would result in \result <== listener != null;, // because the postcondition needs to be open for strengthening in subtypes. // This extra information doesn't help us.

A typical subtype specification would say that the listener is of a given subtype of java.util.EventListener. E.g.:

 ...
 /*@

Specifications: pure
     also

 public behavior

requires listener != null;



Specifications inherited from overridden method in interface ListenerValidity:

 public behavior

requires listener != null;

isEmpty

public final boolean isEmpty()

Specifications: pure

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

add

public final void add(java.util.EventListener 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.

Specifications:

public behavior
requires listener != null ==> isValidListener(listener);
assignable listeners;
ensures listener != null ==> listeners.equals(\old(listeners.insert(listener)));
ensures_redundantly listener != null ==> listeners.has(listener);

remove

public final void remove(java.util.EventListener 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.

Specifications:

public behavior
assignable listeners;
ensures listeners.equals(\old(listeners.remove(listener)));
ensures_redundantly !listeners.has(listener);

isModelFor

public static boolean isModelFor(org.jmlspecs.models.JMLObjectSet jmlSet,
                                 java.util.Set javaSet)

jmlSet and javaSet contain the same elements.

Specifications:

public behavior
requires jmlSet != null;
requires javaSet != null;
ensures \result <==> ( \forall Object o; javaSet.contains(o); jmlSet.has(o))&&( \forall Object o; jmlSet.has(o); javaSet.contains(o));

fireEvent

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

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.

Specifications:

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

toString

public java.lang.String toString()

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

Specifications: pure