|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectjartege.FloatingValue
This class allows one manipulate floating values.
Method Summary | |
static double |
createDouble(long sign,
long mantissa,
long exponent)
Create a double number given the specified sign, mantissa and exponent. |
static float |
createFloat(int sign,
int mantissa,
int exponent)
Create a float number given the specified sign, mantissa and exponent. |
static long |
exponent(double f)
Returns the exponent of double f. |
static int |
exponent(int bits)
Returns the exponent of float represented according to the IEEE 754 floating point format bit layout. |
static long |
exponent(long bits)
Returns the exponent of a double represented according to the IEEE 754 floating point double format bit layout. |
static long |
mantissa(double f)
Returns the mantissa of a double f. |
static int |
mantissa(int bits)
Returns the mantissa of float represented according to the IEEE 754 floating point format bit layout. |
static long |
mantissa(long bits)
Returns the mantissa of a double represented according to the IEEE 754 floating point double format bit layout. |
static double |
nextDouble(double f)
Returns the least double strictly greater than the specified double. |
static float |
nextFloat(float f)
Returns the least float strictly greater than the specified float. |
static double |
previousDouble(double f)
Returns the greatest double strictly less than the specified double. |
static float |
previousFloat(float f)
Returns the greatest float strictly less than the specified float. |
static long |
sign(double f)
Returns 0 if double f is positive, 1 if double f is negative. |
static int |
sign(int bits)
Returns the sign of float represented according to the IEEE 754 floating point format bit layout. |
static long |
sign(long bits)
Returns the sign bit of a double represented according to the IEEE 754 floating point double format bit layout. |
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Method Detail |
public static double createDouble(long sign, long mantissa, long exponent)
requires 0 <= sign && sign <= 1 ; requires 0 <= mantissa && mantissa < 1L << 52 ; requires 0 <= exponent && exponent < 2047 ; ensures sign == 0 ==> (createDouble(0, 0, exponent) <= \result && \result < createDouble(0, 0, exponent + 1)) ; ensures sign == 1 ==> (-createDouble(0, 0, exponent + 1) < \result && \result <= -createDouble(0, 0, exponent)) ;
public static long exponent(long bits)
ensures 0 <= \result && \result <= 2047 ;
public static long exponent(double f)
ensures 0 <= \result && \result <= 2046 ; ensures \result == 0 ==> Math.abs(f) < createDouble(0, 0, 1) ; ensures \result != 0 ==> createDouble(0, 0, \result) <= Math.abs(f) ; ensures \result != 0 && \result != 2046 ==> Math.abs(f) < createDouble(0, 0, \result + 1) ;
public static long sign(long bits)
ensures 0 <= \result && \result <= 1 ;
public static long sign(double f)
ensures 0 <= \result && \result <= 1 ;
public static long mantissa(long bits)
ensures 0 <= \result && \result < 1L << 52 ;
public static long mantissa(double f)
ensures 0 <= \result && \result < 1L << 52 ;
public static double nextDouble(double f)
requires f != Double.MAX_VALUE ; ensures f < \result && (\forall double x ; f < x ; \result <= x) ; ensures previousDouble(\result) == f ;
public static double previousDouble(double f)
requires f != -Double.MAX_VALUE ; ensures \result < f && (\forall double x ; x < f ; x <= \result) ; ensures nextDouble(\result) == f ;
public static float createFloat(int sign, int mantissa, int exponent)
requires 0 <= sign && sign <= 1 ; requires 0 <= mantissa && mantissa < 1 << 23 ; requires 0 <= exponent && exponent < 255 ; ensures sign == 0 ==> (createFloat(0, 0, exponent) <= \result && \result < createFloat(0, 0, exponent + 1)) ; ensures sign == 1 ==> (-createFloat(0, 0, exponent + 1) < \result && \result <= -createFloat(0, 0, exponent)) ;
public static int exponent(int bits)
ensures 0 <= \result && \result <= 255 ;
public static int sign(int bits)
ensures 0 <= \result && \result <= 1 ;
public static int mantissa(int bits)
ensures 0 <= \result && \result < 1 << 23 ;
public static float nextFloat(float f)
requires f != Float.MAX_VALUE ; ensures f < \result && (\forall float x ; f < x ; \result <= x) ; ensures previousFloat(\result) == f ;
public static float previousFloat(float f)
requires f != -Float.MAX_VALUE ; ensures \result < f && (\forall float x ; x < f ; x <= \result) ; ensures nextFloat(\result) == f ;
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |