org.multijava.util
Class ArrayListCache

java.lang.Object
  org.multijava.util.ArrayListCache

public final class ArrayListCache

extends java.lang.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 java.util.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(java.util.ArrayList al)           Adds the given ArrayList back to the cache.
static java.util.ArrayList	request()           Returns an empty ArrayList of default capacity.
static java.util.ArrayList	request(int size)           Returns an empty ArrayList whose capacity is at least of the given size.
static java.util.ArrayList	request(java.util.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 java.util.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.

ArrayListCache

public ArrayListCache()

request

public static java.util.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 java.util.ArrayList request()

Returns an empty ArrayList of default capacity.

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

request

public static java.util.ArrayList request(java.util.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(java.util.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);