/**
 * A FixedSizeSet is a mutable set of integers drawn from the range [0..7]
 **/
public class FixedSizeSet {
    
    /*@ invariant bits.owner == this; */ 
    /*@ spec_public */ private boolean[] bits;
    
    /**
     * Creates a new, empty FixedSizeSet.
     **/
    public FixedSizeSet() 
    //@ ensures (\forall int i; (0 <= i && i < bits.length) ==> (!bits[i])) 
    //@ ensures bits != null
    //@ ensures bits.length == 8
    {
        bits = new boolean[8]; 
        /*@ set bits.owner = this; */
    }
    
    /**
     * Adds n to this set
     **/
    public void add(int n) 
    //@ requires n >= 0 && n < bits.length
    //@ requires bits != null
    //@ ensures bits[n] == true
    //@ ensures bits != null
    {
        bits[n] = true;
    }
    
    /**
     * Returns true iff n is in this set
     **/
    public boolean contains(int n) 
    //@ requires n >= 0 && n < bits.length
    //@ requires bits != null
    //@ ensures \result == bits[n]
    //@ ensures bits != null
    {
        return bits[n];
    }
    
    /**
     * Unions other into this (this' <= this U other)
     **/
    public void union(FixedSizeSet other) 
    //@ requires other != null
    //@ requires other.bits != null
    //@ requires other.bits.length == bits.length
    //@ requires bits != null
    //@ ensures bits != null
    {
        for (int i = 0; i < bits.length; i++) {
            if (other.bits[i]){
                bits[i] = true;
            }
        }
    }
    
    /**
     * Fill an array with one of two objects, based on whether the index
     * is in this set.
     **/
    public void fillDigits(Object[] digits, Object zero, Object one)
    //@ requires digits != null
    //@ requires digits.length >= bits.length
    //@ requires bits != null
    //@ requires \typeof(digits) == \type(Object[])
    //@ ensures bits != null
    {
        for (int i = 0; i < bits.length; i++) {
            Object digit = (bits[i] ? one : zero);
            digits[i] = digit;
        }
    }
    
    /**
     * Return true iff this set represents the same abstract value as
     * the argument, which must be of the same type.
     **/
    public boolean similar(FixedSizeSet other) throws RuntimeException
    //@ requires bits != null
    //@ requires (other != null) ==> other.bits != null
    //@ requires (other != null) ==> other.bits.length == bits.length
    //@ exsures (RuntimeException) other == null
    //@ ensures other != null
    //@ ensures bits != null
    {
        if (other == null){
            throw new RuntimeException("null");
        }
        for (int i = 0; i < bits.length; i++) {
            if (bits[i] != other.bits[i]){
                return false;
            }
        }
        return true;
    }
    
}