java.lang
Class Integer

java.lang.Object
  java.lang.Number
      java.lang.Integer

All Implemented Interfaces:

Comparable, Serializable

public final class Integer

extends Number

implements Comparable

JML's specification of java.lang.Integer.

Version:

$Revision: 1.21 $

Author:

Brandon Shilling, Gary T. Leavens

Class Specifications

public represents theInteger <- this.intValue();

Specifications inherited from class Object

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

Specifications inherited from interface Comparable

instance public invariant ( \forall java.lang.Comparable x; x != null; x.compareTo(x) == 0); instance public invariant ( \forall java.lang.Comparable x, y; x != null&&y != null&&this.definedComparison(x,y)&&this.definedComparison(y,x); this.sgn(x.compareTo(y)) == -this.sgn(y.compareTo(x))); instance public invariant ( \forall int n; n == -1||n == 1; ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(y,z)&&this.definedComparison(x,z); this.sgn(x.compareTo(y)) == n&&this.sgn(y.compareTo(z)) == n ==> this.sgn(x.compareTo(z)) == n)); instance public invariant ( \forall int n; n == -1||n == 1; ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(y,z)&&this.definedComparison(x,z); (this.sgn(x.compareTo(y)) == 0&&this.sgn(y.compareTo(z)) == n||this.sgn(x.compareTo(y)) == n&&this.sgn(y.compareTo(z)) == 0) ==> this.sgn(x.compareTo(z)) == n)); instance public invariant ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(x,z)&&this.definedComparison(y,z); this.sgn(x.compareTo(y)) == 0 ==> this.sgn(x.compareTo(z)) == this.sgn(y.compareTo(z)));

Model Field Summary
int	theInteger

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
(package private) static char[]	DigitOnes
(package private) static char[]	digits
(package private) static char[]	DigitTens
static int	MAX_VALUE
static int	MIN_VALUE
static Class	TYPE

 

Constructor Summary

Integer(int value)

Integer(String s)

 

Model Method Summary
static boolean	decodeable(String nm)
static boolean	parseable(String s)
static boolean	parseable(String s, int r)

 

Model methods inherited from class java.lang.Object

hashValue

 

Model methods inherited from interface java.lang.Comparable

definedComparison, sgn

 

Method Summary
byte	byteValue()
int	compareTo(non_null Integer anotherInteger)
int	compareTo(non_null Object o)
static Integer	decode(non_null String nm)
double	doubleValue()
boolean	equals(nullable Object obj)
float	floatValue()
static Integer	getInteger(String nm)
static Integer	getInteger(String nm, int val)
static Integer	getInteger(String nm, Integer val)
int	hashCode()
int	intValue()
long	longValue()
static int	parseInt(String s)
static int	parseInt(String s, int radix)
short	shortValue()
static String	toBinaryString(int i)
static String	toHexString(int i)
static String	toOctalString(int i)
String	toString()
static String	toString(int i)
static String	toString(int i, int radix)
static Integer	valueOf(String s)
static Integer	valueOf(String s, int radix)

 

Methods inherited from class java.lang.Object

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

 

Model Field Detail

theInteger

public int theInteger

MIN_VALUE

public static final int MIN_VALUE

MAX_VALUE

public static final int MAX_VALUE

TYPE

public static final Class TYPE

Specifications: non_null

digits

static final char[] digits

Specifications: non_null

DigitTens

static final char[] DigitTens

Specifications: non_null

DigitOnes

static final char[] DigitOnes

Specifications: non_null

Integer

public Integer(int value)

Specifications: (class)pure

public normal_behavior
assignable theInteger;
ensures this.theInteger == value;

Integer

public Integer(String s)
        throws NumberFormatException

Throws:

NumberFormatException

Specifications: (class)pure

public normal_behavior
requires parseable(s);
assignable theInteger;
ensures this.theInteger == parseInt(s);

     also

public exceptional_behavior
requires !parseable(s);
signals (java.lang.NumberFormatException) true;

parseable

public static boolean parseable(String s)

Specifications: pure

public normal_behavior
ensures \result == parseable(s,10);

parseable

public static boolean parseable(String s,
                                int r)

Specifications: pure

public normal_behavior
requires 2 <= r&&r <= 36;
ensures \result <==> s != null&&!s.equals("")&&( \forall int i; 0 <= i&&i < s.length(); java.lang.Character.digit(s.charAt(i),r) != -1);

     also

public normal_behavior
requires 2 <= r&&r <= 36;
ensures \result <==> s != null&&!s.equals("")&&( \forall int i; 1 <= i&&i < s.length()&&s.charAt(0) == 45; java.lang.Character.digit(s.charAt(i),r) != -1);

decodeable

public static boolean decodeable(String nm)

Specifications: pure

public normal_behavior
requires nm.length() > 0;

{|

requires (nm.length() >= 2&&nm.charAt(0) == 79&&nm.charAt(1) == 120);
ensures \result == parseable(nm.substring(2),16);

also

requires (nm.length() >= 3&&nm.charAt(0) == 45&&nm.charAt(1) == 79&&nm.charAt(2) == 120);
ensures \result == parseable(nm.substring(3),16);

also

requires (nm.charAt(0) == 35);
ensures \result == parseable(nm.substring(1),16);

also

requires (nm.length() >= 2&&nm.charAt(0) == 45&&nm.charAt(1) == 35);
ensures \result == parseable(nm.substring(2),16);

also

requires (nm.charAt(0) == 79);
ensures \result == parseable(nm.substring(1),8);

also

requires (nm.length() >= 2&&nm.charAt(0) == 45&&nm.charAt(1) == 79);
ensures \result == parseable(nm.substring(2),8);

also

requires !((nm.length() >= 2&&nm.charAt(0) == 79&&nm.charAt(1) == 120)||(nm.length() >= 3&&nm.charAt(0) == 45&&nm.charAt(1) == 79&&nm.charAt(2) == 120)||(nm.charAt(0) == 35)||(nm.length() >= 2&&nm.charAt(0) == 45&&nm.charAt(1) == 35)||(nm.charAt(0) == 79)||(nm.length() >= 2&&nm.charAt(0) == 45&&nm.charAt(1) == 79));
ensures \result == parseable(nm);

|}

toString

public static String toString(int i,
                              int radix)

Specifications: pure non_null

public normal_behavior

{|

requires (2 <= radix&&radix <= 36);

{|

requires i < 0;
ensures \result != null&&\result .length() >= 2&&\result .charAt(0) == 45&&\result .charAt(1) != 48&&i == parseInt(\result ,radix);

also

requires i > 0;
ensures \result != null&&\result .length() >= 1&&\result .charAt(0) != 48&&i == parseInt(\result ,radix);

also

requires i == 0;
ensures "0".equals(\result );

|}

also

requires (2 > radix&&radix > 36);

{|

requires i < 0;
ensures \result != null&&\result .length() >= 2&&\result .charAt(0) == 45&&\result .charAt(1) != 48&&i == parseInt(\result ,10);

also

requires i > 0;
ensures \result != null&&\result .length() >= 1&&\result .charAt(0) != 48&&i == parseInt(\result ,10);

also

requires i == 0;
ensures \result != null&&\result .length() == 1&&\result .charAt(0) == 48;

|}

|}

    implies_that

public normal_behavior
ensures (* \result is a string representation of i in specified radix or default radix *);

    for_example

public normal_example
requires i == -34;
ensures \result != null&&\result .equals("-34");

toHexString

public static String toHexString(int i)

Specifications: pure non_null

public normal_behavior

{|

old int mask_i = (int)(i+4294967296);
requires i < 0&&i != -2147483648;
ensures \result != null&&\result .length() >= 1&&\result .charAt(1) != 48;
ensures \result .equals(toHexString(mask_i));

also

requires i == -2147483648;
ensures \result .equals("80000000");

also

requires i == 0;
ensures \result != null&&\result .length() == 1&&\result .charAt(0) == 48;

also

requires i > 0;
ensures \result != null&&\result .length() >= 1&&\result .charAt(0) != 48&&i == parseInt(\result ,16);

|}

    implies_that

public normal_behavior
ensures (* \result is a string representation of i in hexidecimal *);

toOctalString

public static String toOctalString(int i)

Specifications: pure non_null

public normal_behavior

{|

old int mask_i = (int)(i+4294967296);
requires i < 0&&i != -2147483648;
ensures \result != null&&\result .length() >= 1&&\result .charAt(1) != 48;
ensures \result .equals(toOctalString(mask_i));

also

requires i == -2147483648;
ensures \result .equals("20000000000");

also

requires i == 0;
ensures \result != null&&\result .length() >= 1&&\result .charAt(0) == 48&&\result .length() == 1;

also

requires i > 0;
ensures \result != null&&\result .length() >= 1&&\result .charAt(0) != 48&&i == parseInt(\result ,8);

|}

    implies_that

public normal_behavior
ensures (* \result is a string representation of i in octal *);

toBinaryString

public static String toBinaryString(int i)

Specifications: pure non_null

public normal_behavior

{|

old int mask_i = (int)(i+4294967296);
requires i < 0&&i != -2147483648;
ensures \result != null&&\result .length() >= 1&&\result .charAt(1) != 48;
ensures \result .equals(toBinaryString(mask_i));

also

requires i == -2147483648;
ensures \result .equals("10000000000000000000000000000000");

also

requires i == 0;
ensures "0".equals(\result );

also

requires i > 0;
ensures \result != null&&\result .length() >= 1&&\result .charAt(0) != 48&&i == parseInt(\result ,2);

|}

    implies_that

public normal_behavior
ensures (* \result is a string representation of i in binary *);

toString

public static String toString(int i)

Specifications: pure non_null

public normal_behavior
ensures \result .equals(toString(i,10));

parseInt

public static int parseInt(String s,
                           int radix)
                    throws NumberFormatException

Throws:

NumberFormatException

Specifications: pure

public normal_behavior
requires parseable(s,radix);
ensures (* \result is the int of the string representation in the specified radix *);

     also

public exceptional_behavior
requires !parseable(s,radix);
signals_only java.lang.NumberFormatException;

parseInt

public static int parseInt(String s)
                    throws NumberFormatException

Throws:

NumberFormatException

Specifications: pure

public normal_behavior
requires parseable(s);
ensures \result == parseInt(s,10);

     also

public exceptional_behavior
requires !parseable(s);
signals_only java.lang.NumberFormatException;

valueOf

public static Integer valueOf(String s,
                              int radix)
                       throws NumberFormatException

Throws:

NumberFormatException

Specifications: pure non_null

public normal_behavior
requires parseable(s,radix);
ensures \fresh(\result );

     also

public exceptional_behavior
requires !parseable(s,radix);
signals_only java.lang.NumberFormatException;

valueOf

public static Integer valueOf(String s)
                       throws NumberFormatException

Throws:

NumberFormatException

Specifications: pure non_null

public normal_behavior
requires parseable(s);
ensures \fresh(\result );

     also

public exceptional_behavior
requires !parseable(s);
signals_only java.lang.NumberFormatException;

byteValue

public byte byteValue()

Overrides:

byteValue in class Number

Specifications: (class)pure

     also

public normal_behavior
ensures \result == (byte)this.theInteger;

Specifications inherited from overridden method in class Number:
       pure

public normal_behavior
ensures (* \result is an byte approximation to the value of this object *);

shortValue

public short shortValue()

Overrides:

shortValue in class Number

Specifications: (class)pure

     also

public normal_behavior
ensures \result == (short)this.theInteger;

Specifications inherited from overridden method in class Number:
       pure

public normal_behavior
ensures (* \result is an short approximation to the value of this object *);

intValue

public int intValue()

Specifications: pure

     also

public normal_behavior
ensures \result == this.theInteger;

Specifications inherited from overridden method in class Number:
       pure

public normal_behavior
ensures (* \result is an int approximation to the value of this object *);

longValue

public long longValue()

Specifications: (class)pure

     also

public normal_behavior
ensures \result == this.theInteger;

Specifications inherited from overridden method in class Number:
       pure

public normal_behavior
ensures (* \result is an long approximation to the value of this object *);

floatValue

public float floatValue()

Specifications: (class)pure

     also

public normal_behavior
ensures \result == this.theInteger;

Specifications inherited from overridden method in class Number:
       pure

public normal_behavior
ensures (* \result is an float approximation to the value of this object *);

doubleValue

public double doubleValue()

Specifications: (class)pure

     also

public normal_behavior
ensures \result == this.theInteger;

Specifications inherited from overridden method in class Number:
       pure

public normal_behavior
ensures (* \result is an double approximation to the value of this object *);

toString

public String toString()

Overrides:

toString in class Object

Specifications: non_null (class)pure

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;

hashCode

public int hashCode()

Overrides:

hashCode in class Object

Specifications: (class)pure

     also

public normal_behavior
ensures \result == this.theInteger;

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;

equals

public boolean equals(nullable Object obj)

Overrides:

equals in class Object

Specifications: (class)pure

     also

public normal_behavior
requires obj != null&&(obj instanceof java.lang.Integer);
ensures \result == (this.theInteger == ((java.lang.Integer)obj).intValue());

     also

public normal_behavior
requires obj == null||!(obj instanceof java.lang.Integer);
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 ;

getInteger

public static Integer getInteger(String nm)

Specifications: pure

public normal_behavior
ensures (\result == null&&getInteger(nm,null) == null)||\result .equals(getInteger(nm,null));

getInteger

public static Integer getInteger(String nm,
                                 int val)

Specifications: pure

public normal_behavior
ensures \result .equals(getInteger(nm,new java.lang.Integer(val)));

getInteger

public static Integer getInteger(String nm,
                                 Integer val)

Specifications: pure

public normal_behavior
requires nm != null&&!nm.equals("")&&java.lang.System.getProperty(nm) != null&&decodeable(java.lang.System.getProperty(nm));
ensures \result .equals(decode(java.lang.System.getProperty(nm)));

     also

public normal_behavior
requires nm == null||nm.equals("")||java.lang.System.getProperty(nm) == null||!decodeable(java.lang.System.getProperty(nm));
ensures \result == val||\result .equals(val);

    implies_that

ensures val != null ==> \result != null;

decode

public static Integer decode(non_null String nm)
                      throws NumberFormatException

Throws:

NumberFormatException

Specifications: pure non_null

public normal_behavior
requires decodeable(nm);
ensures (* \result is a Integer representation of nm *);

     also

public exceptional_behavior
requires !decodeable(nm);
signals (java.lang.NumberFormatException) true;

compareTo

public int compareTo(non_null Integer anotherInteger)

Specifications: (class)pure

public normal_behavior
requires anotherInteger != null;

{|

requires this.theInteger == anotherInteger.intValue();
ensures \result == 0;

also

requires this.theInteger < anotherInteger.intValue();
ensures \result < 0;

also

requires this.theInteger > anotherInteger.intValue();
ensures \result > 0;

|}

Specifications inherited from overridden method compareTo(Object o) in interface Comparable:
       pure

public behavior
requires o != null;
ensures (* \result is negative if this is "less than" o *);
ensures (* \result is 0 if this is "equal to" o *);
ensures (* \result is positive if this is "greater than" o *);
signals_only java.lang.ClassCastException;
signals (java.lang.ClassCastException) (* the class of o prohibits it from being compared to this *);

     also

public behavior
requires o != null&&o instanceof java.lang.Comparable;
ensures this.definedComparison((java.lang.Comparable)o,this);
ensures o == this ==> \result == 0;
ensures this.sgn(\result ) == -this.sgn(((java.lang.Comparable)o).compareTo(this));
signals (java.lang.ClassCastException) !this.definedComparison((java.lang.Comparable)o,this);

compareTo

public int compareTo(non_null Object o)

Specified by:

compareTo in interface Comparable

Specifications: (class)pure

     also

public normal_behavior
requires o != null&&(o instanceof java.lang.Integer);
ensures \result == this.compareTo((java.lang.Integer)o);

     also

public exceptional_behavior
requires o == null&&!(o instanceof java.lang.Integer);
signals (java.lang.ClassCastException) true;

Specifications inherited from overridden method compareTo(Object o) in interface Comparable:
       pure

public behavior
requires o != null;
ensures (* \result is negative if this is "less than" o *);
ensures (* \result is 0 if this is "equal to" o *);
ensures (* \result is positive if this is "greater than" o *);
signals_only java.lang.ClassCastException;
signals (java.lang.ClassCastException) (* the class of o prohibits it from being compared to this *);

     also

public behavior
requires o != null&&o instanceof java.lang.Comparable;
ensures this.definedComparison((java.lang.Comparable)o,this);
ensures o == this ==> \result == 0;
ensures this.sgn(\result ) == -this.sgn(((java.lang.Comparable)o).compareTo(this));
signals (java.lang.ClassCastException) !this.definedComparison((java.lang.Comparable)o,this);