org.jutil.event
Interface ListenerValidity

All Known Subinterfaces:

ApplicabilityNotifier, EventTypeReliancy, ListenerTypeReliancy, Notifier, NullEventReliancy

All Known Implementing Classes:

EventSourceSupport

public interface ListenerValidity

This model type introduces a model method which can be used to describe the validity of EventListener instances in a class.

Field Summary
static java.lang.String	CVS_REVISION

 

Method Summary

abstract  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.

 

Field Detail

CVS_REVISION

public static final java.lang.String CVS_REVISION

isValidListener

public abstract 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. // 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

 public behavior

requires listener != null;