JML

org.multijava.util
Class ArrayListCache

java.lang.Object
  extended byorg.multijava.util.ArrayListCache

public final class ArrayListCache
extends Object

This class implements a cache of ArrayLists. It is an efficiency hack to reduce the amount of object allocation and garbage collection do to short-term use of ArrayLists. This class is _not_ synchronized.


Field Summary
private static ArrayList[] cacheArray
          The cache of instantiated but currently unused ArrayList objects.
private static int cacheSize
           
private static int DEFAULT_LIST_CAPACITY
           
(package private) static int MIN_CACHE_SIZE
           
private static int pos
          The highest index of a non-null object in the cache.
private static int shrinkAtSize
           
 
Constructor Summary
ArrayListCache()
           
 
Method Summary
private static void growCache()
          Increases the cache capacity.
static void release(ArrayList al)
          Adds the given ArrayList back to the cache.
static ArrayList request()
          Returns an empty ArrayList of default capacity.
static ArrayList request(int size)
          Returns an empty ArrayList whose capacity is at least of the given size.
static ArrayList request(Collection content)
          Returns an ArrayList whose initial contents are the given collection.
private static void shrinkCache()
          Reduces the cache capacity.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

MIN_CACHE_SIZE

static final int MIN_CACHE_SIZE

DEFAULT_LIST_CAPACITY

private static final int DEFAULT_LIST_CAPACITY

cacheArray

private static ArrayList[] cacheArray
The cache of instantiated but currently unused ArrayList objects.


cacheSize

private static int cacheSize

shrinkAtSize

private static int shrinkAtSize

pos

private static int pos
The highest index of a non-null object in the cache.

Constructor Detail

ArrayListCache

public ArrayListCache()
Method Detail

request

public static ArrayList request(int size)
Returns an empty ArrayList whose capacity is at least of the given size.

 requires size > 0;
 modifies cache;
 ensures \result != null && !\reach(ArrayListCache.class).has(\result);
 


request

public static ArrayList request()
Returns an empty ArrayList of default capacity.

 modifies cache;
 ensures \result != null && !\reach(ArrayListCache.class).has(\result);
 


request

public static ArrayList request(Collection content)
Returns an ArrayList whose initial contents are the given collection.

 requires content != null;
 modifies cache;
 ensures \result != null && !\reach(ArrayListCache.class).has(\result);
 


release

public static void release(ArrayList al)
Adds the given ArrayList back to the cache. Clients should not clear the list before releasing it, as this method handles that. This method promises not to grab aliases to the list members.

 requires al != null;
 modifies cache;
 ensures al.isEmpty() && 
   \reach(\old(al)).intersection(\reach(ArrayListCache.class)).isEmpty();
 


shrinkCache

private static void shrinkCache()
Reduces the cache capacity.

 requires pos < shrinkAtSize && cacheSize > MIN_CACHE_SIZE;
 ensures cacheSize < \old(cacheSize);
 


growCache

private static void growCache()
Increases the cache capacity.

 ensures cacheSize > \old(cacheSize);
 


JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.