listenertypereliancy.jml

一个关于java 的常用工具包

package org.jutil.event;


import java.util.EventListener;


/**
 * <p>This model type states that only listeners of type
 *   {@link listenerType} are considered valid. It can be used in
 *   conjunction with {@link EventSourceSupport} or {@link Notifier}, who
 *   also model implement ListenerValidity, or one of their subtypes.</p>
 * <p>If your class should only accept listeners of type
 *   {@link listenerType} as valid events, you can simply model
 *   implement this type to inherit that contract. The implementation of
 *   {@link EventSourceSupport#fireEvent(EventObject, Notifier)} or {@link
 *   Notifier#notifyListener(EventListener, EventObject)} then can
 *   depend on the fact that its listener argument will be of
 *   type {@link listenerType}, because {#isValidListener(EventListener)}
 *   method is used as an abstract precondition by those methods.</p>
 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.
 *
 * @path    $Source: /cvsroot/org-jutil/jutil.org/src/org/jutil/event/ListenerTypeReliancy.jml,v $
 * @version $Revision: 1.6 $
 * @date    $Date: 2002/09/08 14:47:11 $
 * @state   $State: Exp $
 * @author  Jan Dockx
 * @release $Name:  $
 */
public interface ListenerTypeReliancy extends ListenerValidity {

  /* The revision of this class */
	public final static String CVS_REVISION ="$Revision: 1.6 $";

  public invariant listenerType != null;
  public invariant Class.forName("java.util.EventListener").isAssignableFrom(listenerType);
/*  public invariant EventListener.class.isAssignableFrom(listenerType);
      doesn't work in jml, but it doesn't work in java either. For some weird
      reason .class doesn't work with interfaces, only with classes.
      Class.forName() works for everything. */

  public model instance Class listenerType;

  /**
   * Asserts that <formal-arg>listener</formal-arg> is of type
   * {@link listenerType}. Subtypes cannot demand more.
   */
 /*@
   @ also public behavior
   @
   @ pre listener != null;
   @
   @ post \result <==> listenerType.isInstance(listener);
   @*/
  public pure model boolean isValidListener(EventListener listener);
    // final because the contract states an equivalence
    // FIXME

}

/*<copyright>Copyright (C) 1997-2001. This software is copyrighted by 
the people and entities mentioned after the "@author" tags above, on 
behalf of the JUTIL.ORG Project. The copyright is dated by the dates 
after the "@date" tags above. All rights reserved.
This software is published under the terms of the JUTIL.ORG Software
License version 1.1 or later, a copy of which has been included with
this distribution in the LICENSE file, which can also be found at
http://org-jutil.sourceforge.net/LICENSE. This software is distributed WITHOUT 
ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 
or FITNESS FOR A PARTICULAR PURPOSE. See the JUTIL.ORG Software 
License for more details.
For more information, please see http://org-jutil.sourceforge.net/</copyright>*/