/*
 * Written by Doug Lea with assistance from members of JCP JSR-166
 * Expert Group and released to the public domain. Use, modify, and
 * redistribute this code in any way without acknowledgement.
 */

package java.util.concurrent;
import java.util.*;

/**
 * A {@link java.util.Set} that uses {@link
 * java.util.concurrent.CopyOnWriteArrayList} for all of its
 * operations.  Thus, it shares the same basic properties:
 * <ul>
 *  <li>It is best suited for applications in which set sizes generally
 *       stay small, read-only operations
 *       vastly outnumber mutative operations, and you need
 *       to prevent interference among threads during traversal.
 *  <li>Mutative operations(add, set, remove, etc) are expensive
 *      since they usually entail copying the entire underlying array.
 *  <li>Iterators do not support the mutative remove operation
 *  <li>Traversal via iterators is very fast and cannot ever encounter
 *      interference from other threads. Iterators rely on
 *      unchanging snapshots of the array at the time the iterators were
 *     constructed.
 * </ul>
 * <p>
 * <b>Sample Usage.</b> Probably the main application
 * of copy-on-write sets are classes that maintain
 * sets of Handler objects
 * that must be multicasted to upon an update command. This
 * is a classic case where you do not want to be holding a
 * lock while sending a message, and where traversals normally
 * vastly overwhelm additions.
 * <pre>
 * class Handler { void handle(); ... }
 *
 * class X {
 *    private final CopyOnWriteArraySet&lt;Handler&gt; handlers = new CopyOnWriteArraySet&lt;Handler&gt;();
 *    public void addHandler(Handler h) { handlers.add(h); }
 *
 *    private long internalState;
 *    private synchronized void changeState() { internalState = ...; }
 *
 *    public void update() {
 *       changeState();
 *       Iterator it = handlers.iterator();
 *       while (it.hasNext())
 *          it.next().handle();
 *    }
 * }
 * </pre>
 * @see CopyOnWriteArrayList
 *
 * <p>This class is a member of the
 * <a href="{@docRoot}/../guide/collections/index.html">
 * Java Collections Framework</a>.
 *
 * @since 1.5
 * @author Doug Lea
 * @param <E> the type of elements held in this collection
 */
public class CopyOnWriteArraySet<E> extends AbstractSet<E>
		implements Cloneable, java.io.Serializable {
	private static final long serialVersionUID = 5457747651344034263L;

	private /*@ spec_public rep @*/ final CopyOnWriteArrayList<E> al;

	/**
	 * Creates an empty set.
	 */
	/*@ public normal_behavior
	   @   ensures \independent && \fresh(al);
	   @*/
	public /*@ atomic @*/ CopyOnWriteArraySet() {
		al = new CopyOnWriteArrayList<E>();
	}

	/**
	 * Creates a set containing all of the elements of the specified
	 * Collection.
	 * @param c the collection
	 */
	/*@ public normal_behavior
	   @   requires \thread_safe(c) && c != null;
	   @   ensures \fresh(al.array) && (\forall Object o; c.contains(o);
	   @                    (\exists int i; i >= 0 && i < al.array.length;
	   @                       o == al.array[i] || (o != null && o.equals(al.array[i]))));
	   @*/
	public /*@ atomic @*/ CopyOnWriteArraySet(Collection<? extends E> c) {
		al = new CopyOnWriteArrayList<E>();
		al.addAllAbsent(c);
	}


	/*@ public normal_behavior
	   @   assignable \nothing;
	   @   ensures \result == al.array.length;
	   @*/
	public /*@ atomic @*/ int      size()                    { return al.size(); }
	
	/*@ public normal_behavior
	   @   assignable \nothing;
	   @   ensures \result <==> (al.array.length == 0);
	   @*/
	public /*@ atomic @*/ boolean  isEmpty()                 { return al.isEmpty(); }
	
	/*@ public normal_behavior
	   @   assignable \nothing;
	   @   ensures (al.array == \old(al.array)) ==>
	   @                 \result <==> (\exists int i; i >= 0 && i < al.array.length; elem.equals(al.array[i])); 
	   @*/
	public /*@ atomic @*/ boolean  contains(Object o)        { return al.contains(o); }
	
	//@ ensures \fresh(\result) && (al.array == \old(al.array) ==>
	//@                                        (\forall int i; i >= 0 && i < al.array.length;
	//@                                            al.array[i].equals(\result[i])));
	public /*@ atomic @*/ Object[] toArray()                 { return al.toArray(); }
	
	/*@ public normal_behavior
	   @   requires a != null && \elemtype(\typeof(a)) :> \elemtype(\typeof(al.array));
	   @   ensures (al.array == \old(al.array)) ==>
	   @                  ((a.length >= al.array.length) ==> 
	   @                       (\forall int i; i >= 0 && i < al.array.length; al.array[i].equals(a[i]))) &&
	   @                  ((a.length < al.array.length) ==> \fresh(a) && a.length == al.array.length &&
	   @                       (\forall int i; i >= 0 && i < al.array.length; al.array[i].equals(a[i])));
	   @also
	   @ public exceptional_behavior
	   @   requires a == null;
	   @   signals (Exception npe) npe instanceof NullPointerException;
	   @also
	   @ public exceptional_behavior
	   @   requires !(\elemtype(\typeof(a)) :> \elemtype(\typeof(al.array)));
	   @   signals (Exception ase) ase instanceof ArrayStoreException;
	   @*/	
	public /*@ atomic @*/ <T> T[]  toArray(T[] a)            { return al.toArray(a); }
	
	/*@ public normal_behavior
	   @   locks al;
	   @   ensures \fresh(al.array) && al.array.length == 0;
	   @*/
	public /*@ atomic @*/void     clear()                   {        al.clear(); }
	
	//@ ensures \fresh(\result) && \independent;
	public /*@ atomic @*/ Iterator<E>  iterator()            { return al.iterator(); }
	
	/*@ public normal_behavior
	   @   locks al;
	   @   assignable al.array;
	   @   ensures ((\exists int i; i >= 0 && i < \old(al.array.length);
	   @                   (o == \old(al.array[i]) || (o != null && \old(al.array[i]).equals(o))) &&
	   @                    (\forall int j; j >= 0 && j < i; \old(al.array[j]) == al.array[j]) &&
	   @                    (\forall int j; j >= i && j < al.array.length; al.array[i] == \old(al.array[i + 1])) &&
	   @                     al.array.length == \old(al.array.length) - 1) ==> \result) &&
	   @                (!(\exists int i; i >= 0 && i < \old(al.array.length);
	   @                   (o == \old(al.array[i]) || (o != null && \old(al.array[i]).equals(o)))) ==>
	   @                      !(\result) && al.array.length == \old(al.array.length));
	   @*/
	public /*@ atomic @*/ boolean  remove(Object o)          { return al.remove(o); }
	
	/*@ public normal_behavior
	   @   locks al;
	   @   ensures (!(exists int i; i >= 0 && i < al.array.length;
	   @                    element == \old(al.array[i]) || (element != null && element.equals(\old(al.array[i])))) ==>
	   @                      (al.array.length == \old(al.array.length) + 1 &&
	   @                      (\forall int i; i >= 0 && i < al.array.length -1; al.array[i] == \old(al.array[i])) &&
	   @                      al.array[al.array.length - 1] == element && \result)) &&
	   @               (exists int i; i >= 0 && i < al.array.length;
	   @                    element == \old(al.array[i]) || (element != null && element.equals(\old(al.array[i])))) ==>
	   @                      (al.array == \old(al.array) && !(\result));
	   @*/
	public /*@ atomic @*/ boolean  add(E o)                  { return al.addIfAbsent(o); }
	
	/*@ public normal_behavior
	   @   requires \thread_safe(c) && c != null;
	   @   ensures (al.array == \old(al.array)) ==>
	   @                 (\result <==> (\forall Object o; c.contains(o);
	   @                    (\exists int i; i >= 0 && i < al.array.length;
	   @                       o == al.array[i] || (o != null && o.equals(al.array[i])))));
	   @*/	
	public /*@ atomic @*/ boolean  containsAll(Collection<?> c)      { return al.containsAll(c); }
	
	/*@ public normal_behavior
	   @   requires \thread_safe(c) && c != null;
	   @   locks al;
	   @   ensures \result <==> c.size() > 0;
	   @   ensures (\forall Object o; c.contains(o);
	   @                   (\exits int i; i >= \old(al.array.length) && i < \old(al.array.length) + c.size();
	   @                            o == al.array[i] || (o != null && o.equals(al.array[i])))) &&
	   @               al.array.length == \old(al.array.length) + c.size() &&
	   @               (\forall int i; i >= 0 && i < \old(al.array.length); al.array[i] == \old(al.array[i]));
	   @*/	
	public /*@ atomic @*/ boolean  addAll(Collection<? extends E> c) { return al.addAllAbsent(c) > 0; }
	
	/*@ public normal_behavior
	   @   requires \thread_safe(c) && c != null;
	   @   locks al;
	   @   ensures \result <==> !(\not_modified(al.array));
	   @   ensures (\forall Object o; c.contains(o);
	   @                    !(\exists int i; i >= 0 && i < al.array.length;
	   @                          o == al.array[i] || (o != null && o.equals(al.array[i]))));
	   @*/	
	public /*@ atomic @*/ boolean  removeAll(Collection<?> c)        { return al.removeAll(c); }
	
	/*@ public normal_behavior
	   @   requires \thread_safe(c) && c != null;
	   @   locks al;
	   @   ensures \result <==> !(\not_modified(al.array));
	   @   ensures (\forall int i; i >= 0 && i < al.array.length;
	   @                   c.contans(al.array[i]));
	   @*/
	public /*@ atomic @*/ boolean  retainAll(Collection<?> c)        { return al.retainAll(c); }

}