java.lang
Class Double

java.lang.Object
  java.lang.Number
      java.lang.Double

All Implemented Interfaces:

Comparable, Serializable

public final class Double

extends Number

implements Comparable

JML's specification of java.lang.Double.

Version:

$Revision: 1.19 $

Author:

Brandon Shilling, David R. Cok, Gary T. Leavens

Class Specifications

represents theDouble <- this.doubleValue();

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
double	theDouble

 

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
static double	MAX_VALUE
static double	MIN_VALUE
static double	NaN
static double	NEGATIVE_INFINITY
static double	POSITIVE_INFINITY
static Class	TYPE

 

Constructor Summary

Double(double value)

Double(non_null String s)

 

Model Method Summary
static boolean	identical(double a, double b)           Returns true if a and b represent the same double value; the usual == does not work to distinguish positive and negative zeros or to identify two NaN values as equal.
static boolean	isNegativeZero(double a)           Returns true if the argument is a negative (and not positive) zero; the usual == returns true for comparing positive and negative zero.
static boolean	isPositiveZero(double a)           Returns true if the argument is a positive (and not negative) zero; the usual == returns true for comparing positive and negative zero.
static boolean	parseable(String s)           Returns true if the string is a parseable double value (but not an infinite or NaN value).

 

Model methods inherited from class java.lang.Object

hashValue

 

Model methods inherited from interface java.lang.Comparable

definedComparison, sgn

 

Method Summary
byte	byteValue()
static int	compare(double d1, double d2)
int	compareTo(non_null Double anotherDouble)
int	compareTo(non_null Object o)
static long	doubleToLongBits(double value)
static long	doubleToRawLongBits(double value)
double	doubleValue()
boolean	equals(nullable Object obj)
float	floatValue()
int	hashCode()
int	intValue()
boolean	isInfinite()
static boolean	isInfinite(double v)
boolean	isNaN()
static boolean	isNaN(double v)
static double	longBitsToDouble(long bits)
long	longValue()
static double	parseDouble(non_null String s)
short	shortValue()
String	toString()
static String	toString(double d)
static Double	valueOf(non_null String s)

 

Methods inherited from class java.lang.Object

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

 

Model Field Detail

theDouble

public double theDouble

POSITIVE_INFINITY

public static final double POSITIVE_INFINITY

NEGATIVE_INFINITY

public static final double NEGATIVE_INFINITY

NaN

public static final double NaN

MAX_VALUE

public static final double MAX_VALUE

MIN_VALUE

public static final double MIN_VALUE

TYPE

public static final Class TYPE

Specifications: non_null

Double

public Double(double value)

Specifications: (class)pure

public normal_behavior
assignable theDouble;
ensures identical(this.theDouble,value);

Double

public Double(non_null String s)
       throws NumberFormatException

Throws:

NumberFormatException

Specifications: (class)pure

public normal_behavior
requires parseable(s);
assignable theDouble;
ensures identical(this.theDouble,parseDouble(s));

     also

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

parseable

public static boolean parseable(String s)

Returns true if the string is a parseable double value (but not an infinite or NaN value).

Specifications: pure

public normal_behavior
requires s != null;

{|

requires s.equals("NaN");
ensures !\result ;

also

requires s.equals("");
ensures !\result ;

also

requires s.equals("Infinity")||s.equals("-Infinity");
ensures !\result ;

also

requires s.equals("0.0")||s.equals("-0.0");
ensures \result ;

also

requires (* parseable to a floating-point double by the IEEE 754 standards *);
ensures \result ;

also

requires !(* parseable to a floating-point double by the IEEE 754 standards *);
ensures !\result ;

|}

isNegativeZero

public static boolean isNegativeZero(double a)

Returns true if the argument is a negative (and not positive) zero; the usual == returns true for comparing positive and negative zero.

Specifications: pure

isPositiveZero

public static boolean isPositiveZero(double a)

Returns true if the argument is a positive (and not negative) zero; the usual == returns true for comparing positive and negative zero.

Specifications: pure

identical

public static boolean identical(double a,
                                double b)

Returns true if a and b represent the same double value; the usual == does not work to distinguish positive and negative zeros or to identify two NaN values as equal.

Specifications: pure

toString

public static String toString(double d)

Specifications: pure non_null

public normal_behavior
ensures !isNaN(d)&&!isInfinite(d) ==> parseable(\result );
ensures !isNaN(d)&&!isInfinite(d) ==> identical(d,parseDouble(\result ));
ensures isNaN(d) ==> \result .equals("NaN");
ensures (d == Infinity) ==> \result .equals("Infinity");
ensures (d == -Infinity) ==> \result .equals("-Infinity");

valueOf

public static Double valueOf(non_null String s)
                      throws NumberFormatException

Throws:

NumberFormatException

Specifications: pure non_null

public normal_behavior
requires s != null&&parseable(s);
ensures \result .equals(new java.lang.Double(parseDouble(s)));

     also

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

parseDouble

public static double parseDouble(non_null String s)
                          throws NumberFormatException

Throws:

NumberFormatException

Specifications: pure

public normal_behavior
requires s != null&&parseable(s);
ensures true;

     also

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

isNaN

public static boolean isNaN(double v)

Specifications: pure

public normal_behavior
ensures \result == !(v == v);

isInfinite

public static boolean isInfinite(double v)

Specifications: pure

public normal_behavior
ensures \result <==> (v == Infinity||v == -Infinity);

isNaN

public boolean isNaN()

Specifications: (class)pure

public normal_behavior
ensures \result == !(this.theDouble == this.theDouble);

isInfinite

public boolean isInfinite()

Specifications: (class)pure

public normal_behavior
ensures \result == (this.theDouble == Infinity||this.theDouble == -Infinity);

toString

public String toString()

Overrides:

toString in class Object

Specifications: non_null (class)pure

     also

ensures \result .equals(toString(this.doubleValue()));

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;

byteValue

public byte byteValue()

Overrides:

byteValue in class Number

Specifications: (class)pure

     also

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

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.theDouble;

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: (class)pure

     also

public normal_behavior
ensures \result == (int)this.theDouble;

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 == (long)this.theDouble;

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 java.lang.Float.identical(\result ,(float)this.theDouble);

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 identical(\result ,this.theDouble);

Specifications inherited from overridden method in class Number:
       pure

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

hashCode

public int hashCode()

Overrides:

hashCode in class Object

Specifications: (class)pure

     also

public normal_behavior
ensures (* \result is a hashcode value for this 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;

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.Double);
ensures \result == identical(this.theDouble,((java.lang.Double)obj).doubleValue());

     also

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

doubleToLongBits

public static long doubleToLongBits(double value)

Specifications: pure

public normal_behavior

{|

requires value == Infinity;
ensures \result == 9218868437227405312;

also

requires value == -Infinity;
ensures \result == -4503599627370496;

also

requires isNaN(value);
ensures \result == 9221120237041090560;

also

ensures (* \result is the bits that represent the floating-point number *);

also

ensures identical(value,longBitsToDouble(doubleToLongBits(value)));

|}

    implies_that

public normal_behavior
requires !isNaN(value);
ensures longBitsToDouble(\result ) == value;

doubleToRawLongBits

public static long doubleToRawLongBits(double value)

Specifications: pure

public normal_behavior

{|

requires value == Infinity;
ensures \result == 9218868437227405312;

also

requires value == -Infinity;
ensures \result == -4503599627370496;

also

requires isNaN(value);
ensures (* is the long integer representing the actual NaN value *);

also

ensures (* \result is the bits that represent the floating-point number *);

also

ensures identical(value,longBitsToDouble(doubleToRawLongBits(value)));

|}

    implies_that

public normal_behavior
requires !isNaN(value);
ensures longBitsToDouble(\result ) == value;

longBitsToDouble

public static double longBitsToDouble(long bits)

Specifications: pure

public normal_behavior

{|

requires bits == 9218868437227405312;
ensures \result == Infinity;

also

requires bits == -4503599627370496;
ensures \result == -Infinity;

also

requires (9218868437227405313 <= bits&&bits <= 9223372036854775807)||(-4503599627370495 <= bits&&bits <= -1);
ensures isNaN(\result );

also

ensures (* \result is floating-point value with the same bit pattern as bits *);

|}

compareTo

public int compareTo(non_null Double anotherDouble)

Specifications: (class)pure

public normal_behavior
requires anotherDouble != null;

{|

requires anotherDouble.isNaN()&&this.isNaN();
ensures \result == 0;

also

requires this.isNaN()&&!anotherDouble.isNaN();
ensures \result > 0;

also

requires !this.isNaN()&&anotherDouble.isNaN();
ensures \result < 0;

also

requires isPositiveZero(this.theDouble)&&isNegativeZero(anotherDouble.doubleValue());
ensures \result > 0;

also

requires isNegativeZero(this.theDouble)&&isPositiveZero(anotherDouble.doubleValue());
ensures \result < 0;

also

requires !(anotherDouble.isNaN()||this.isNaN())&&!(isPositiveZero(this.theDouble)&&isNegativeZero(anotherDouble.doubleValue()))&&!(isNegativeZero(this.theDouble)&&isPositiveZero(anotherDouble.doubleValue()));

{|

requires this.theDouble < anotherDouble.doubleValue();
ensures \result < 0;

also

requires this.theDouble == anotherDouble.doubleValue();
ensures \result == 0;

also

requires this.theDouble > anotherDouble.doubleValue();
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.Double);
ensures \result == this.compareTo((java.lang.Double)o);

     also

public exceptional_behavior
requires o == null||!(o instanceof java.lang.Double);
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);

compare

public static int compare(double d1,
                          double d2)

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result == new java.lang.Double(d1).compareTo(new java.lang.Double(d2));