org.jutil.event
Interface EventTypeReliancy
- All Superinterfaces:
- ListenerValidity, Notifier
- All Known Implementing Classes:
- TypeApplicabilityNotifier
- public interface EventTypeReliancy
- extends Notifier
This model type extends the Notifier contract, stating that only
non-null events of type eventType are considered
valid.
If your notifier only accepts non-null events of type
eventType as valid events, you can simply model implement
this type to inherit that contract. The implementation of
Notifier#notifyListner(EventListener, EventObject) then can
depend on the fact that it's event argument will be non-null and of
type eventType, because this method is used as an
abstract precondition.
These extra contracts only make sense if they introduce an implication
if the form \result <== something (or a fortiori, an equivalence).
We need to prove in the use of the actual notifyListener method,
i.e., in the fireEvent method, that we adhere to the preconditions, i.e.,
that this model methode returns true. An implication of the form
\result ==> something leaves room for strengthening in subclasses,
but we can only proof that the method returns false in some conditions.
We cannot proof that the method will return true ever.
| Class Specifications |
public invariant eventType != null;
public invariant Class.forName("java.util.EventObject").isAssignableFrom(eventType); |
|
Model Field Summary |
java.lang.Class |
eventType
|
|
Method Summary |
abstract boolean |
isValidEvent(java.util.EventObject event)
Asserts that event is of type
eventType. |
eventType
public java.lang.Class eventType
- Specifications: instance
isValidEvent
public abstract boolean isValidEvent(java.util.EventObject event)
- Asserts that event is of type
eventType. Subtypes cannot demand more.
- Specifications: pure
- also
-
public behavior
ensures \result <==> eventType.isInstance(event);
- Specifications inherited from overridden method in interface Notifier:
--- None ---