org.jutil.event
Interface Notifier

All Superinterfaces:

ListenerValidity

All Known Subinterfaces:

ApplicabilityNotifier, EventTypeReliancy, NullEventReliancy

All Known Implementing Classes:

ChainNotifier

public interface Notifier

extends ListenerValidity

Notifier instances are used to call the correct call-back method defined in a listener type when EventSourceSupport fires events. The method EventSourceSupport.fireEvent(EventObject, Notifier) presents the event to the notifier for each listener that is registered in the EventSourceSupport instance. This technique is similar to the well-known double-dispatch.

Abstract preconditions are used to transport information about the listener and the event from clients, over type invariants, to the implementation of notifyEventListener(EventListener, EventObject). An abstract postcondition makes it possible for EventSourceSupport to specify that notifyEventListener(EventListener, EventObject) is actually called.

Most often, this interface is implemented in an inner class of the actual event source that used the EventSourceSupport instance. A typical implementation looks like this:

 ...
 static final private Notifier _eventNameNotifier =
     new Notifier() {
           /oo
            o also
            o   public behavior
            o     post \result <==> (event != null) && (event instanceof EventNameEvent);
            o public model boolean isValidEvent(EventObject event);
            o/
           /oo
            o also
            o   public behavior
            o     pre listener != null;
            o     post \result <==> (listener instanceof EventNameListener);
            o public model boolean isValidListener(EventListener listener);
            o/
           /oo
            o also
            o   public behavior
            o     pre listener != null;
            o     pre isValidListener(listener);
            o     pre isValidEvent(event);
            o     post (* ((EventNameListener)listener).eventName((EventNameEvent)event)
            o             is called *);
            o/
           public void notifyEventListener(EventListener listener, EventObject event) {
             ((EventNameListener)listener).eventName((EventNameEvent)event);
           }
         };
 ...
 

EventTypeReliancy and ListenerTypeReliance offer support for the case where the validity of events or listeners is only limited to type.

In the above example, the notifier instance has no state, and can thus be stored in a final class variable, for use in all event firings. An event firing typically looks like this:

 public void fooMutator(arguments) { 
   store old state
   do mutation
   EventNameEvent event = create new event using old and new state;
   $eventNameEventSourceSupport.fireEvent(event, _eventNameNotifier);
 }
 

In case more elaborate firing mechanisms are needed, different notifiers can be created in the actual event source class, potentially as instance variables with state, potentially as inner classes in the mutator method, so that they have access to the full context of the mutator. If the $eventNameEventSourceSupport is used to store listeners of different types, a chain of responsibility of notifiers can be used (see ChainNotifier).

ApplicabilityNotifier adds the possibility to check the applicability of a notifier in particular listener/event combinations at runtime. TypeApplicabilityNotifier adds specification that makes it more easy to specify that listeners and events of a particular type are valid.

Field Summary
static java.lang.String	CVS_REVISION

 

Method Summary
abstract  boolean	isValidEvent(java.util.EventObject event)           This model inspector can be used to transport information about the event argument of notifyEventListener from the actual event source providing the event to the class implementing this interface.
abstract  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.
abstract  boolean	notifyEventListenerCalled(java.util.EventListener listener, java.util.EventObject event)           This model inspector is an abstract postcondition for notifyEventListener(EventListener, EventObject).

 

Methods inherited from interface org.jutil.event.ListenerValidity

isValidListener

 

Field Detail

CVS_REVISION

public static final java.lang.String CVS_REVISION

isValidEvent

public abstract boolean isValidEvent(java.util.EventObject event)

This model inspector can be used to transport information about the event argument of notifyEventListener from the actual event source providing the event to the class implementing this interface.

Specifications: pure

notifyEventListener

public abstract 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. This is used in EventSourceSupport to specify that this method will indeed be called by EventSourceSupport.fireEvent(EventObject, Notifier).

Specifications:

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);

notifyEventListenerCalled

public abstract boolean notifyEventListenerCalled(java.util.EventListener listener,
                                                  java.util.EventObject event)

This model inspector is an abstract postcondition for notifyEventListener(EventListener, EventObject). It can be used by clients to specify that notifyEventListener(EventListener, EventObject) is indeed called.

This is used in EventSourceSupport to specify that notifyEventListener(EventListener, EventObject) will be called by EventSourceSupport.fireEvent(EventObject, Notifier). Because that class can only talk about this type, and not about a specific subtype where the abstract postcondition is elaborated, the abstract postcondition can only be made true by actually calling notifyEventListener(EventListener, EventObject).

This techique depends on the Java limitation of not allowing covariant argument type strengthening. Otherwise, the EventSourceSupport.fireEvent(EventObject, Notifier) could be strengthened in a subclass of EventSourceSupport to only accept notifiers of a subtype of this interface, where a new method could be added that uses this model method as abstract postcondition also. That class could implement EventSourceSupport.fireEvent(EventObject, Notifier) correctly then by calling that new method on all listeners, instead of notifyEventListener(EventListener, EventObject).

This cannot be replaced with a model field, because if it was: in this type, there is no method that says it is assignable, except notifyEventListener, which sets it to true. So, we can conclude that, once we used this notifier to notify a listener, it never becomes false again. So, the postcondition of the fireEvent method is trivially true for all future events. Second note: this probably isn't true: we need the event/listener combination, and we only can get that with a method anyway. In any case, this would prohibit sending the same event twice.

Specifications: pure

public behavior
requires listener != null;
requires isValidListener(listener);
requires isValidEvent(event);