jartege
Class FloatingValue

java.lang.Object
  extended byjartege.FloatingValue

public class FloatingValue
extends java.lang.Object

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

createDouble

public static double createDouble(long sign,
                                  long mantissa,
                                  long exponent)
Create a double number given the specified sign, mantissa and 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)) ; 
    
 


exponent

public static long exponent(long bits)
Returns the exponent of a double represented according to the IEEE 754 floating point double format bit layout.


 ensures 
    0 <= \result && \result <= 2047 ; 

 


exponent

public static long exponent(double f)
Returns the exponent of 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) ; 

 


sign

public static long sign(long bits)
Returns the sign bit of a double represented according to the IEEE 754 floating point double format bit layout. Returns 0 if the double if positive, 1 if the double is negative.


 ensures
    0 <= \result && \result <= 1 ;

 


sign

public static long sign(double f)
Returns 0 if double f is positive, 1 if double f is negative.


 ensures
    0 <= \result && \result <= 1 ;

 


mantissa

public static long mantissa(long bits)
Returns the mantissa of a double represented according to the IEEE 754 floating point double format bit layout.


 ensures
    0 <= \result && \result < 1L << 52 ;

 


mantissa

public static long mantissa(double f)
Returns the mantissa of a double f.


 ensures
    0 <= \result && \result < 1L << 52 ;

 


nextDouble

public static double nextDouble(double f)
Returns the least double strictly greater than the specified double.


 requires
    f != Double.MAX_VALUE ; 

 ensures
    f < \result && (\forall double x ; f < x ; \result <= x) ; 

 ensures
   previousDouble(\result) == f ; 

 


previousDouble

public static double previousDouble(double f)
Returns the greatest double strictly less than the specified double.


 requires
    f != -Double.MAX_VALUE ;

 ensures
    \result < f && (\forall double x ; x < f ; x <= \result) ;

 ensures
    nextDouble(\result) == f ; 

 


createFloat

public static float createFloat(int sign,
                                int mantissa,
                                int exponent)
Create a float number given the specified sign, mantissa and 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)) ; 

 


exponent

public static int exponent(int bits)
Returns the exponent of float represented according to the IEEE 754 floating point format bit layout.


 ensures
    0 <= \result && \result <= 255 ;

 


sign

public static int sign(int bits)
Returns the sign of float represented according to the IEEE 754 floating point format bit layout. Returns 0 if the float is positive, 1 if the float is negative.


 ensures
    0 <= \result && \result <= 1 ; 

 


mantissa

public static int mantissa(int bits)
Returns the mantissa of float represented according to the IEEE 754 floating point format bit layout.


 ensures
    0 <= \result && \result < 1 << 23 ;

 


nextFloat

public static float nextFloat(float f)
Returns the least float strictly greater than the specified float.


 requires
    f != Float.MAX_VALUE ; 

 ensures
    f < \result && (\forall float x ; f < x ; \result <= x) ; 

 ensures
    previousFloat(\result) == f ; 

 


previousFloat

public static float previousFloat(float f)
Returns the greatest float strictly less than the specified float.


 requires
    f != -Float.MAX_VALUE ;

 ensures
    \result < f && (\forall float x ; x < f ; x <= \result) ;

 ensures
    nextFloat(\result) == f ;