java.util
Class BitSet

java.lang.Object
  java.util.BitSet

All Implemented Interfaces:

Cloneable, Serializable

public class BitSet

extends Object

implements Cloneable, Serializable

JML's specification of the java.util.BitSet. We imagine a bitset as a set of integers, which are the ones whose bits are true in the BitSet.

Version:

$Revision: 1.11 $

Author:

Gary T. Leavens

Class Specifications

public invariant this.capacity >= 0; public invariant ( \forall java.lang.Object o; this.trueBits.has(o); o instanceof org.jmlspecs.models.JMLInteger&&0 <= ((org.jmlspecs.models.JMLInteger)o).intValue()&&((org.jmlspecs.models.JMLInteger)o).intValue() < this.capacity); public represents trueBits <- this.abstractValue();

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary
int	capacity
JMLValueSet	trueBits

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Constructor Summary

BitSet()

BitSet(int nbits)

 

Model Method Summary
JMLValueSet	abstractValue()

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	and(BitSet set)
void	andNot(BitSet set)
int	cardinality()
void	clear()
void	clear(int bitIndex)
void	clear(int fromIndex, int toIndex)
Object	clone()
boolean	equals(nullable Object obj)
void	flip(int bitIndex)
void	flip(int fromIndex, int toIndex)
boolean	get(int bitIndex)
BitSet	get(int fromIndex, int toIndex)
int	hashCode()
boolean	intersects(BitSet set)
boolean	isEmpty()
int	length()
int	nextClearBit(int fromIndex)
int	nextSetBit(int fromIndex)
void	or(BitSet set)
void	set(int bitIndex)
void	set(int bitIndex, boolean value)
void	set(int fromIndex, int toIndex)
void	set(int fromIndex, int toIndex, boolean value)
int	size()
String	toString()
void	xor(BitSet set)

 

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

 

Model Field Detail

capacity

public int capacity

trueBits

public JMLValueSet trueBits

Specifications: non_null

BitSet

public BitSet()

Specifications: pure

public normal_behavior
assignable trueBits, capacity;
ensures this.trueBits.isEmpty();

BitSet

public BitSet(int nbits)

Specifications: pure

public normal_behavior
requires nbits >= 0;
assignable trueBits, capacity;
ensures this.trueBits.isEmpty()&&this.capacity == nbits;

     also

public exceptional_behavior
requires nbits < 0;
assignable \nothing;
signals_only java.lang.NegativeArraySizeException;

abstractValue

public JMLValueSet abstractValue()

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result != null&&( \forall int i; ; \result .has(new org.jmlspecs.models.JMLInteger(i)) <==> this.get(i));

flip

public void flip(int bitIndex)

Specifications:

public normal_behavior
requires bitIndex >= 0;

{|

assignable capacity, trueBits;
ensures this.capacity >= \old(this.capacity)&&this.capacity >= bitIndex;

also

requires !this.trueBits.has(new org.jmlspecs.models.JMLInteger(bitIndex));
assignable capacity, trueBits;
ensures this.trueBits.equals(\old(this.trueBits.insert(new org.jmlspecs.models.JMLInteger(bitIndex))));

also

requires this.trueBits.has(new org.jmlspecs.models.JMLInteger(bitIndex));
assignable capacity, trueBits;
ensures this.trueBits.equals(\old(this.trueBits.remove(new org.jmlspecs.models.JMLInteger(bitIndex))));

|}

     also

public exceptional_behavior
requires bitIndex < 0;
assignable \nothing;
signals_only java.lang.IndexOutOfBoundsException;

flip

public void flip(int fromIndex,
                 int toIndex)

Specifications:

public normal_behavior
requires 0 <= fromIndex&&toIndex <= toIndex;
assignable capacity, trueBits;
ensures this.capacity >= \old(this.capacity)&&this.capacity >= toIndex;
ensures this.trueBits.equals(\old(this.trueBits.difference( new org.jmlspecs.models.JMLValueSet { org.jmlspecs.models.JMLInteger i | this.trueBits.has(i) && fromIndex <= i.intValue()&&i.intValue() < toIndex }).union( new org.jmlspecs.models.JMLValueSet { org.jmlspecs.models.JMLInteger i | org.jmlspecs.models.JMLModelValueSet.JMLIntegers().has(i) && !this.trueBits.has(i)&&fromIndex <= i.intValue()&&i.intValue() < toIndex })));

     also

public exceptional_behavior
requires !(0 <= fromIndex&&fromIndex <= toIndex);
assignable \nothing;
signals_only java.lang.IndexOutOfBoundsException;

set

public void set(int bitIndex)

Specifications:

public normal_behavior
requires bitIndex >= 0;
assignable capacity, trueBits;
ensures this.capacity >= \old(this.capacity)&&this.capacity >= bitIndex;
ensures this.trueBits.equals(\old(this.trueBits.insert(new org.jmlspecs.models.JMLInteger(bitIndex))));

     also

public exceptional_behavior
requires bitIndex < 0;
assignable \nothing;
signals_only java.lang.IndexOutOfBoundsException;

set

public void set(int bitIndex,
                boolean value)

Specifications:

public normal_behavior
requires bitIndex >= 0;

{|

assignable capacity, trueBits;
ensures this.capacity >= \old(this.capacity)&&this.capacity >= bitIndex;

also

requires value;
assignable capacity, trueBits;
ensures this.trueBits.equals(\old(this.trueBits.insert(new org.jmlspecs.models.JMLInteger(bitIndex))));

also

requires !value;
assignable capacity, trueBits;
ensures this.trueBits.equals(\old(this.trueBits.remove(new org.jmlspecs.models.JMLInteger(bitIndex))));

|}

     also

public exceptional_behavior
requires bitIndex < 0;
assignable \nothing;
signals_only java.lang.IndexOutOfBoundsException;

set

public void set(int fromIndex,
                int toIndex)

Specifications:

public normal_behavior
requires 0 <= fromIndex&&toIndex <= toIndex;
assignable capacity, trueBits;
ensures this.capacity >= \old(this.capacity)&&this.capacity >= toIndex;
ensures this.trueBits.equals(\old(this.trueBits.union( new org.jmlspecs.models.JMLValueSet { org.jmlspecs.models.JMLInteger i | org.jmlspecs.models.JMLModelValueSet.JMLIntegers().has(i) && fromIndex <= i.intValue()&&i.intValue() < toIndex })));

     also

public exceptional_behavior
requires !(0 <= fromIndex&&toIndex <= toIndex);
assignable \nothing;
signals_only java.lang.IndexOutOfBoundsException;

set

public void set(int fromIndex,
                int toIndex,
                boolean value)

Specifications:

public normal_behavior
requires 0 <= fromIndex&&toIndex <= toIndex;

{|

assignable capacity, trueBits;
ensures this.capacity >= \old(this.capacity)&&this.capacity >= toIndex;

also

requires value;
assignable capacity, trueBits;
ensures this.trueBits.equals(\old(this.trueBits.union( new org.jmlspecs.models.JMLValueSet { org.jmlspecs.models.JMLInteger i | org.jmlspecs.models.JMLModelValueSet.JMLIntegers().has(i) && fromIndex <= i.intValue()&&i.intValue() < toIndex })));

also

requires !value;
assignable capacity, trueBits;
ensures this.trueBits.equals(\old(this.trueBits.difference( new org.jmlspecs.models.JMLValueSet { org.jmlspecs.models.JMLInteger i | org.jmlspecs.models.JMLModelValueSet.JMLIntegers().has(i) && fromIndex <= i.intValue()&&i.intValue() < toIndex })));

|}

     also

public exceptional_behavior
requires !(0 <= fromIndex&&toIndex <= toIndex);
assignable \nothing;
signals_only java.lang.IndexOutOfBoundsException;

clear

public void clear(int bitIndex)

Specifications:

public normal_behavior
requires bitIndex >= 0;
assignable capacity, trueBits;
ensures this.capacity >= \old(this.capacity)&&this.capacity >= bitIndex;
ensures this.trueBits.equals(\old(this.trueBits.remove(new org.jmlspecs.models.JMLInteger(bitIndex))));

     also

public exceptional_behavior
requires bitIndex < 0;
assignable \nothing;
signals_only java.lang.IndexOutOfBoundsException;

clear

public void clear(int fromIndex,
                  int toIndex)

Specifications:

public normal_behavior
requires 0 <= fromIndex&&toIndex <= toIndex;
assignable capacity, trueBits;
ensures this.capacity >= \old(this.capacity)&&this.capacity >= toIndex;
ensures this.trueBits.equals(\old(this.trueBits.difference( new org.jmlspecs.models.JMLValueSet { org.jmlspecs.models.JMLInteger i | org.jmlspecs.models.JMLModelValueSet.JMLIntegers().has(i) && fromIndex <= i.intValue()&&i.intValue() < toIndex })));

     also

public exceptional_behavior
requires !(0 <= fromIndex&&toIndex <= toIndex);
assignable \nothing;
signals_only java.lang.IndexOutOfBoundsException;

clear

public void clear()

Specifications:

public normal_behavior
assignable capacity, trueBits;
ensures this.trueBits.isEmpty();

get

public boolean get(int bitIndex)

Specifications: pure

public normal_behavior
requires bitIndex >= 0;
assignable \nothing;
ensures \result <==> this.trueBits.has(new org.jmlspecs.models.JMLInteger(bitIndex));

     also

public exceptional_behavior
requires bitIndex < 0;
signals_only java.lang.IndexOutOfBoundsException;

get

public BitSet get(int fromIndex,
                  int toIndex)

Specifications: pure

public normal_behavior
requires 0 <= fromIndex&&toIndex <= toIndex;
assignable \nothing;
ensures \result != null&&( \forall int i; ; \result .trueBits.has(new org.jmlspecs.models.JMLInteger(i)) <==> fromIndex <= i&&i < toIndex);

     also

public exceptional_behavior
requires !(0 <= fromIndex&&toIndex <= toIndex);
assignable \nothing;
signals_only java.lang.IndexOutOfBoundsException;

nextSetBit

public int nextSetBit(int fromIndex)

Specifications: pure

public normal_behavior
requires fromIndex >= 0;

{|

requires ( \exists int i; ; fromIndex <= i&&this.trueBits.has(new org.jmlspecs.models.JMLInteger(i)));
assignable \nothing;
ensures \result == ( \min int i; fromIndex <= i&&this.trueBits.has(new org.jmlspecs.models.JMLInteger(i)); i);

also

requires !( \exists int i; ; fromIndex <= i&&this.trueBits.has(new org.jmlspecs.models.JMLInteger(i)));
assignable \nothing;
ensures \result == -1;

|}

     also

public exceptional_behavior
requires fromIndex < 0;
assignable \nothing;
signals_only java.lang.IndexOutOfBoundsException;

nextClearBit

public int nextClearBit(int fromIndex)

Specifications: pure

public normal_behavior
requires fromIndex >= 0;

{|

requires ( \exists int i; ; fromIndex <= i&&!this.trueBits.has(new org.jmlspecs.models.JMLInteger(i)));
assignable \nothing;
ensures \result == ( \min int i; fromIndex <= i&&!this.trueBits.has(new org.jmlspecs.models.JMLInteger(i)); i);

also

requires !( \exists int i; ; fromIndex <= i&&this.trueBits.has(new org.jmlspecs.models.JMLInteger(i)));
assignable \nothing;
ensures \result == -1;

|}

     also

public exceptional_behavior
requires fromIndex < 0;
assignable \nothing;
signals_only java.lang.IndexOutOfBoundsException;

length

public int length()

Specifications: pure

public normal_behavior

{|

requires !this.trueBits.isEmpty();
assignable \nothing;
ensures \result == 1+( \max int i; 0 <= i&&this.trueBits.has(new org.jmlspecs.models.JMLInteger(i)); i);

also

requires this.trueBits.isEmpty();
assignable \nothing;
ensures \result == 0;

|}

isEmpty

public boolean isEmpty()

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result <==> this.trueBits.isEmpty();

intersects

public boolean intersects(BitSet set)

Specifications: pure

public normal_behavior
requires set != null;
assignable \nothing;
ensures \result <==> !this.trueBits.intersection(set.trueBits).isEmpty();
ensures_redundantly \result <==> ( \exists int i; 0 <= i; this.trueBits.has(new org.jmlspecs.models.JMLInteger(i))&&set.trueBits.has(new org.jmlspecs.models.JMLInteger(i)));

cardinality

public int cardinality()

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result == ( \num_of int i; 0 <= i; this.trueBits.has(new org.jmlspecs.models.JMLInteger(i)));

and

public void and(BitSet set)

Specifications:

public normal_behavior
requires set != null;
assignable trueBits, capacity;
ensures this.trueBits.equals(\old(this.trueBits.intersection(set.trueBits)));
ensures_redundantly ( \forall int i; 0 <= i&&i < this.length(); this.trueBits.has(new org.jmlspecs.models.JMLInteger(i)) <==> \old(this.trueBits.has(new org.jmlspecs.models.JMLInteger(i))&&set.trueBits.has(new org.jmlspecs.models.JMLInteger(i))));

or

public void or(BitSet set)

Specifications:

public normal_behavior
requires set != null;
assignable trueBits, capacity;
ensures this.trueBits.equals(\old(this.trueBits.union(set.trueBits)));
ensures_redundantly ( \forall int i; 0 <= i&&i < java.lang.Math.max(this.length(),set.length()); this.trueBits.has(new org.jmlspecs.models.JMLInteger(i)) <==> \old(this.trueBits.has(new org.jmlspecs.models.JMLInteger(i))||set.trueBits.has(new org.jmlspecs.models.JMLInteger(i))));

xor

public void xor(BitSet set)

Specifications:

public normal_behavior
requires set != null;
assignable trueBits, capacity;
ensures ( \forall int i; 0 <= i&&i < java.lang.Math.max(this.length(),set.length()); this.trueBits.has(new org.jmlspecs.models.JMLInteger(i)) <==> \old(this.trueBits.has(new org.jmlspecs.models.JMLInteger(i))^set.trueBits.has(new org.jmlspecs.models.JMLInteger(i))));

andNot

public void andNot(BitSet set)

Specifications:

public normal_behavior
requires set != null;
assignable trueBits, capacity;
ensures ( \forall int i; 0 <= i&&i < this.length(); this.trueBits.has(new org.jmlspecs.models.JMLInteger(i)) <==> \old(this.trueBits.has(new org.jmlspecs.models.JMLInteger(i))&!set.trueBits.has(new org.jmlspecs.models.JMLInteger(i))));

hashCode

public int hashCode()

Overrides:

hashCode in class Object

Specifications inherited from overridden method in class Object:

public behavior
assignable objectState;
ensures (* \result is a hash code for this object *);

     also

public code normal_behavior
assignable \nothing;

size

public int size()

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result >= this.length();
ensures_redundantly \result >= 1+( \max int i; 0 <= i&&this.trueBits.has(new org.jmlspecs.models.JMLInteger(i)); i);

equals

public boolean equals(nullable Object obj)

Overrides:

equals in class Object

Specifications: pure

     also

public normal_behavior
requires obj instanceof java.util.BitSet;

{|

old java.util.BitSet s = (java.util.BitSet)obj;
assignable \nothing;
ensures \result <==> this.trueBits.equals(s.trueBits);
ensures_redundantly \result <==> this.length() == s.length()&&( \forall int i; 0 <= i&&i < this.length(); this.trueBits.has(new org.jmlspecs.models.JMLInteger(i)) <==> s.trueBits.has(new org.jmlspecs.models.JMLInteger(i)));

|}

     also

public normal_behavior
requires !(obj instanceof java.util.BitSet);
assignable \nothing;
ensures !\result ;

Specifications inherited from overridden method equals(Object obj) in class Object:
       pure

public normal_behavior
requires obj != null;
ensures (* \result is true when obj is "equal to" this object *);

     also

public normal_behavior
requires this == obj;
ensures \result ;

     also

public code normal_behavior
requires obj != null;
ensures \result <==> this == obj;

     also

diverges false;
ensures obj == null ==> !\result ;

clone

public Object clone()

Overrides:

clone in class Object

Specifications:

     also

public normal_behavior
assignable \nothing;
ensures \fresh(\result )&&this.equals((java.util.BitSet)\result )&&this.size() == ((java.util.BitSet)\result ).size();

Specifications inherited from overridden method in class Object:
       non_null

protected normal_behavior
requires this instanceof java.lang.Cloneable;
assignable \nothing;
ensures \result != null;
ensures \typeof(\result ) == \typeof(this);
ensures (* \result is a clone of this *);

     also

protected normal_behavior
requires this.getClass().isArray();
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((java.lang.Object[])\result ).length == ((java.lang.Object[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((java.lang.Object[])this).length; ((java.lang.Object[])\result )[i] == ((java.lang.Object[])this)[i]);

     also

requires this.getClass().isArray();
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures java.lang.reflect.Array.getLength(\result ) == java.lang.reflect.Array.getLength(this);
ensures ( \forall int i; 0 <= i&&i < java.lang.reflect.Array.getLength(this); ( \exists java.lang.Object result_i; result_i == java.lang.reflect.Array.get(\result ,i); (result_i == null&&java.lang.reflect.Array.get(this,i) == null)||(result_i != null&&result_i.equals(java.lang.reflect.Array.get(this,i)))));

     also

protected exceptional_behavior
requires !(this instanceof java.lang.Cloneable);
assignable \nothing;
signals_only java.lang.CloneNotSupportedException;

     also

protected normal_behavior
requires \elemtype(\typeof(this)) <: \type(java.lang.Object);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((java.lang.Object[])\result ).length == ((java.lang.Object[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((java.lang.Object[])this).length; ((java.lang.Object[])\result )[i] == ((java.lang.Object[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(int);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((int[])\result ).length == ((int[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((int[])this).length; ((int[])\result )[i] == ((int[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(byte);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((byte[])\result ).length == ((byte[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((byte[])this).length; ((byte[])\result )[i] == ((byte[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(char);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((char[])\result ).length == ((char[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((char[])this).length; ((char[])\result )[i] == ((char[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(long);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((long[])\result ).length == ((long[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((long[])this).length; ((long[])\result )[i] == ((long[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(short);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((short[])\result ).length == ((short[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((short[])this).length; ((short[])\result )[i] == ((short[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(boolean);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((boolean[])\result ).length == ((boolean[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((boolean[])this).length; ((boolean[])\result )[i] == ((boolean[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(float);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((float[])\result ).length == ((float[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((float[])this).length; (java.lang.Float.isNaN(((float[])\result )[i])&&java.lang.Float.isNaN(((float[])this)[i]))||((float[])\result )[i] == ((float[])this)[i]);

     also

protected normal_behavior
requires \elemtype(\typeof(this)) == \type(double);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((double[])\result ).length == ((double[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((double[])this).length; (java.lang.Double.isNaN(((double[])\result )[i])&&java.lang.Double.isNaN(((double[])this)[i]))||((double[])\result )[i] == ((double[])this)[i]);

toString

public String toString()

Overrides:

toString in class Object

Specifications inherited from overridden method in class Object:
       non_null

public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);

     also

public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);

     also

public code model_program { ... }

    implies_that

assignable objectState;
ensures \result != null;