// @(#)$Id: HashSet.refines-spec,v 1.14 2006/12/12 00:02:12 chalin Exp $

// Copyright (C) 2005 Iowa State University
//
// This file is part of the runtime library of the Java Modeling Language.
//
// This library is free software; you can redistribute it and/or
// modify it under the terms of the GNU Lesser General Public License
// as published by the Free Software Foundation; either version 2.1,
// of the License, or (at your option) any later version.
//
// This library is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
// Lesser General Public License for more details.
//
// You should have received a copy of the GNU Lesser General Public License
// along with JML; see the file LesserGPL.txt.  If not, write to the Free
// Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA
// 02110-1301  USA.

package java.util;

import org.jmlspecs.models.*;

/** JML's specification of java.util.HashSet.
 * @author Katie Becker
 * @author Gary T. Leavens
 */
public class HashSet extends AbstractSet
    implements Set, Cloneable, java.io.Serializable
{
    //@ public represents addOperationSupported = true;
    //@ public represents removeOperationSupported = true;

    //@ public model int initialCapacity;    
    //@ public model float loadFactor;
    
    //@ public invariant initialCapacity >= 0;  
    //@ public invariant loadFactor > 0;
    
    /*@ public normal_behavior
       @   assignable theSet, initialCapacity, loadFactor;
       @   ensures theSet != null && theSet.isEmpty();
       @   ensures loadFactor == 0.75;
       @   ensures initialCapacity == 16;
       @*/
    public HashSet();

     /*@ public normal_behavior
       @    requires c != null;
       @    assignable theSet, initialCapacity, loadFactor;
       @    ensures loadFactor == 0.75 
       @         && theSet.equals(JMLEqualsSet.convertFrom(c));
       @*/
    public HashSet(Collection c);

     /*@ public normal_behavior
       @    requires initialCapacity >= 0;
       @    assignable theSet, this.initialCapacity, this.loadFactor;
       @    ensures theSet != null && theSet.isEmpty();
       @    ensures this.initialCapacity == initialCapacity
       @         && this.loadFactor == loadFactor;
       @*/ 
    public HashSet(int initialCapacity, float loadFactor);

    /*@ public normal_behavior
       @    assignable theSet, this.initialCapacity, this.loadFactor;
       @    ensures theSet != null && theSet.isEmpty();
       @    ensures this.initialCapacity == initialCapacity
       @         && this.loadFactor == 0.75;
       @*/
    public HashSet(int initialCapacity);

    HashSet(int initialCapacity, float loadFactor, boolean dummy);

    // specified by Set
    //@ pure
    public Iterator iterator();

    // specified by Set
    //@ pure
    public int size();

    // specified by Set
    //@ pure
    public boolean isEmpty();

    // specified by Set
    //@ pure
    public boolean contains(/*@nullable*/ Object o);

    // specified by Set
    public boolean add(/*@nullable*/ Object o);

    // specified by Set
    public boolean remove(/*@nullable*/ Object o);

    // specified by Set
    public void clear();

    /*@ also
       @   public normal_behavior
       @     assignable \nothing;
       @     ensures \result instanceof Set && \fresh(\result)
       @          && ((Set)\result).equals(this);
       @     ensures_redundantly \result != this;
       @*/    
    public Object clone();

    static final long serialVersionUID;
}