robustvisitor.java

一个关于java 的常用工具包

   *         This can be null.
   */
 /*@
   @ // The changes are applied to the given array,
   @ // which is returned afterwards
   @ post \result == array;
   @ // public void visit(Object) is called for all
   @ // elements of <array>.
   @ post (* for all e in collection: visit(e) *);
   @
   @ signals (Exception)
   @         (* Something has gone wrong during the visit *);
   @*/
  public final Object[] applyTo(Object[] array) throws Exception {
		//MvDMvDMvD PRECONDITION !!!
    if (array != null) {
      try {
        int[] dimensions = Arrays.getArrayDimensions(array);
        // Calculate the number of elements in the array.
        int nbElements=1;
        for(int i=0;i<dimensions.length;i++) {
          nbElements = nbElements * dimensions[i];
        }
        List undoDataList = new Vector(nbElements);
        try {
          ObjectArrayIterator iter = new ObjectArrayIterator(array);
          while (! iter.atEnd()) {
            Object element = iter.getElement();
            Object undoData = visit(element);
            undoDataList.add(new Entry(element, undoData));
            iter.next();            
          }
          Object element = iter.getElement();
          Object undoData = visit(element);
          undoDataList.add(new Entry(element, undoData));
        }
        catch(Exception exc) {
          // Only entries for elements that were succesfully visited are 
          // in the list, so we have to call unvisit on all elements.
          ListIterator iter = undoDataList.listIterator();
          // moving the iterator to the end.
          while (iter.hasNext()) {
            iter.next();
          }
          while (iter.hasPrevious()) {
            // The value is the undo data.
            Entry entry = (Entry) iter.previous();
            unvisit(entry.getKey(),entry.getValue());
          }
          throw exc;
        }
      }
      catch(ZeroDimensionException exc) {
        // do nothing
      }
    }    
    return array;
  }
  
  /**
   * <p>Perform the visitation defined in <code>public void visit(Object)</code>
   * on all elements reachable from <iterator>. The contents of the underlying collection
   * is not changed.</p>
   *
   * @param  iterator
   *         The iterator to perform this visitation on. This can be null.
   * @result <code>public void visit(Object)</code> is called for all elements of
   *         <iterator>.
   *       | for all e in iterator: visit(e)
   * @excep  Throwable
   *         Something has gone wrong during the visit.
   */
 /*@
   @ pre (* The iterator must be at the beginning of its iteration. *);
   @
   @ // The iterator will be at the end
   @ post ! iterator.hasNext();
   @
	 @ signals (ConcurrentModificationException) (* The collection was modified while visiting. *);
   @ signals (Exception)
   @         (* Something has gone wrong during the visit *);
   @*/
  public final void applyTo(Iterator iterator) throws Exception, ConcurrentModificationException {
		//MvDMvDMvD PRECONDITION !!!
    if (iterator != null) {
      // not effective, but we can't get the size.
      List undoDataList = new Vector();
      try {
        while (iterator.hasNext()) {
          Object element = iterator.next();
          Object undoData = visit(element);
          undoDataList.add(new Entry(element, undoData));
        }
      }
      catch(Exception exc) {
        // Only entries for elements that were succesfully visited are 
        // in the list, so we have to call unvisit on all elements.
        ListIterator iter = undoDataList.listIterator();
        // moving the iterator to the end :(
        while (iter.hasNext()) {
          iter.next();
        }
        while (iter.hasPrevious()) {
            // The value is the undo data.
            Entry entry = (Entry) iter.previous();
            unvisit(entry.getKey(),entry.getValue());
          }
        throw exc;
      }
    }    
  }  

  /**
   * <p>Perform the visitation defined in <code>public void visit(Object)</code>
   * on all elements reachable from <enumeration>. The contents of the underlying collection
   * is not changed.</p>
   *
   * @param  enumeration
   *         The enumeration to perform this visitation on. This can be null.
   * @result <code>public void visit(Object)</code> is called for all elements of
   *         <iterator>.
   *       | for all e in enumeration: visit(e)
   * @excep  Throwable
   *         Something has gone wrong during the visit.
   */
 /*@
   @ pre (* The enumeration must be at the beginning of its enumeration. *);
   @
   @ // The enumeration will be at the end
   @ post ! enumeration.hasMoreElements();
   @
	 @ signals (ConcurrentModificationException) (* The collection was modified while visiting. *);
   @ signals (Exception)
   @         (* Something has gone wrong during the visit *);
   @*/
  public final void applyTo(Enumeration enumeration) throws Exception, ConcurrentModificationException {
		//MvDMvDMvD PRECONDITION !!!
    if (enumeration != null) {
      // not efficient, but we can't get the size.
      List undoDataList = new Vector();
      try {
        while (enumeration.hasMoreElements()) {
          Object element = enumeration.nextElement();
          Object undoData = visit(element);
          undoDataList.add(new Entry(element, undoData));
        }
      }
      catch(Exception exc) {
        // Only entries for elements that were succesfully visited are 
        // in the list, so we have to call unvisit on all elements.
        ListIterator iter = undoDataList.listIterator();
        // moving the iterator to the end.
        // thx Sun, for this wonderful interface
        while (iter.hasNext()) {
          iter.next();
        }
        while (iter.hasPrevious()) {
            // The value is the undo data.
            Entry entry = (Entry) iter.previous();
            unvisit(entry.getKey(),entry.getValue());
          }
        throw exc;
      }
    }    
  }  
  
    
  class Entry {
    /**
     * Initialize a new Entry with the given key and value.
     */
   /*@
     @ // The key of this Entry is set to <key>.
     @ post getKey() == key;
     @ // The value of this Entry is set to <value>.
     @ post getValue() == value;
     @*/
    public Entry(Object key, Object value) {
      $key=key;
      $value=value;
    }
    
    /**
     * Return the key of this Entry.
     */
    public Object getKey() {
      return $key;
    }

    /**
     * Return the value of this Entry.
     */
    public Object getValue() {
      return $value;
    }

    /**
     * The key of this Entry.
     */
    private Object $key;
    
    /**
     * The value of this Entry.
     */
    private Object $value;
  }
}

/*<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>*/