JML

java.util
Class BitSet

java.lang.Object
  extended byjava.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
Constructor Detail

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;
Model Method Detail

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));
Method Detail

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;

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.