JML

java.lang
Class Float

java.lang.Object
  extended byjava.lang.Number
      extended byjava.lang.Float
All Implemented Interfaces:
Comparable, Serializable

public final class Float
extends Number
implements Comparable

JML's specification of java.lang.Float.

Version:
$Revision: 1.19 $
Author:
Brandon Shilling, David R. Cok, Gary T. Leavens

Class Specifications
public represents theFloat <- this.floatValue();

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
 float theFloat
           
 
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 float MAX_VALUE
           
static float MIN_VALUE
           
static float NaN
           
static float NEGATIVE_INFINITY
           
static float POSITIVE_INFINITY
           
static Class TYPE
           
 
Constructor Summary
Float(double value)
           
Float(float value)
           
Float(String s)
           
 
Model Method Summary
static boolean identical(float a, float 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(float 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(float 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 parseable as a float 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(float f1, float f2)
           
 int compareTo(non_null Float anotherFloat)
           
 int compareTo(non_null Object o)
           
 double doubleValue()
           
 boolean equals(nullable Object obj)
           
static int floatToIntBits(float value)
           
static int floatToRawIntBits(float value)
           
 float floatValue()
           
 int hashCode()
           
static float intBitsToFloat(int bits)
           
 int intValue()
           
 boolean isInfinite()
           
static boolean isInfinite(float v)
           
 boolean isNaN()
           
static boolean isNaN(float v)
           
 long longValue()
           
static float parseFloat(non_null String s)
           
 short shortValue()
           
 String toString()
           
static String toString(float f)
           
static Float valueOf(non_null String s)
           
 
Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
 

Model Field Detail

theFloat

public float theFloat
Field Detail

POSITIVE_INFINITY

public static final float POSITIVE_INFINITY

NEGATIVE_INFINITY

public static final float NEGATIVE_INFINITY

NaN

public static final float NaN

MAX_VALUE

public static final float MAX_VALUE

MIN_VALUE

public static final float MIN_VALUE

TYPE

public static final Class TYPE
Specifications: non_null
Constructor Detail

Float

public Float(float value)
Specifications: (class)pure
public normal_behavior
assignable theFloat;
ensures identical(this.theFloat,value);

Float

public Float(double value)
Specifications: (class)pure
public normal_behavior
assignable theFloat;
ensures identical(this.theFloat,(float)value);

Float

public Float(String s)
      throws NumberFormatException
Throws:
NumberFormatException
Specifications: (class)pure
public normal_behavior
requires parseable(s);
assignable theFloat;
ensures identical(this.theFloat,parseFloat(s));
     also
public exceptional_behavior
requires !parseable(s);
signals (java.lang.NumberFormatException) true;
Model Method Detail

parseable

public static boolean parseable(String s)
Returns true if the string is parseable as a float 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("Infinity")||s.equals("-Infinity");
ensures !\result ;
also
requires s.equals("");
ensures !\result ;
also
requires s.equals("0.0")||s.equals("-0.0");
ensures \result ;
also
requires (* s is parseable to a float by the IEEE 754 standards *);
ensures \result ;
also
requires !(* s is parseable to a float by the IEEE 754 standards *);
ensures !\result ;
|}

isNegativeZero

public static boolean isNegativeZero(float 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(float 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(float a,
                                float 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
Method Detail

toString

public static String toString(float f)
Specifications: pure non_null
public normal_behavior
ensures !isNaN(f)&&!isInfinite(f) ==> parseable(\result );
ensures !isNaN(f)&&!isInfinite(f) ==> identical(f,parseFloat(\result ));
ensures isNaN(f) ==> \result .equals("NaN");
ensures (f == Infinity) ==> \result .equals("Infinity");
ensures (f == -Infinity) ==> \result .equals("-Infinity");

valueOf

public static Float 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.Float(parseFloat(s)));
     also
public exceptional_behavior
requires s != null&&!parseable(s);
signals (java.lang.NumberFormatException) true;

parseFloat

public static float parseFloat(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(float v)
Specifications: pure
public normal_behavior
ensures \result == !(v == v);

isInfinite

public static boolean isInfinite(float v)
Specifications: pure
public normal_behavior
ensures \result == (v == Infinity||v == -Infinity);

isNaN

public boolean isNaN()
Specifications: (class)pure
public normal_behavior
requires true;
ensures \result == !(this.theFloat == this.theFloat);

isInfinite

public boolean isInfinite()
Specifications: (class)pure
public normal_behavior
ensures \result == (this.theFloat == Infinity||this.theFloat == -Infinity);

toString

public String toString()
Overrides:
toString in class Object
Specifications: non_null (class)pure
     also
ensures \result .equals(toString(this.floatValue()));
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.theFloat;
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.theFloat;
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.theFloat;
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.theFloat;
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 identical(this.theFloat,\result );
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 java.lang.Double.identical(this.theFloat,\result );
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.Float);
ensures \result == identical(this.theFloat,((java.lang.Float)obj).floatValue());
     also
public normal_behavior
requires obj != null&&!(obj instanceof java.lang.Float);
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 ;

floatToIntBits

public static int floatToIntBits(float value)
Specifications: pure
public normal_behavior
{|
requires value == Infinity;
ensures \result == 2139095040;
also
requires value == -Infinity;
ensures \result == -8388608;
also
requires new java.lang.Float(value).isNaN();
ensures \result == 2143289344;
also
ensures (* \result is the bits that represent the floating-point number *);
also
ensures identical(value,intBitsToFloat(floatToIntBits(value)));
|}
    implies_that
public normal_behavior
requires !isNaN(value);
ensures intBitsToFloat(\result ) == value;

floatToRawIntBits

public static int floatToRawIntBits(float value)
Specifications: pure
public normal_behavior
{|
requires value == Infinity;
ensures \result == 2139095040;
also
requires value == -Infinity;
ensures \result == -8388608;
also
requires isNaN(value);
ensures (* is the int representing the actual NaN value *);
also
ensures (* \result is the bits that represent the floating-point number *);
also
ensures identical(value,intBitsToFloat(floatToRawIntBits(value)));
|}
    implies_that
public normal_behavior
requires !isNaN(value);
ensures intBitsToFloat(\result ) == value;

intBitsToFloat

public static float intBitsToFloat(int bits)
Specifications: pure
public normal_behavior
{|
requires bits == 2139095040;
ensures \result == Infinity;
also
requires bits == -8388608;
ensures \result == -Infinity;
also
requires (2139095041 <= bits&&bits <= 2147483647)||(-8388607 <= bits&&bits <= -1);
ensures new java.lang.Float(\result ).isNaN();
also
ensures (* \result is floating-point value with the same bit pattern as bits *);
|}

compareTo

public int compareTo(non_null Float anotherFloat)
Specifications: (class)pure
public normal_behavior
requires anotherFloat != null;
{|
requires this.isNaN()&&anotherFloat.isNaN();
ensures \result == 0;
also
requires !this.isNaN()&&anotherFloat.isNaN();
ensures \result < 0;
also
requires this.isNaN()&&!anotherFloat.isNaN();
ensures \result > 0;
also
requires isPositiveZero(this.theFloat)&&isNegativeZero(anotherFloat.floatValue());
ensures \result > 0;
also
requires isNegativeZero(this.theFloat)&&isPositiveZero(anotherFloat.floatValue());
ensures \result < 0;
also
requires !(this.isNaN()||anotherFloat.isNaN())&&!(isPositiveZero(this.theFloat)&&isNegativeZero(anotherFloat.floatValue()))&&!(isNegativeZero(this.theFloat)&&isPositiveZero(anotherFloat.floatValue()));
{|
requires this.theFloat < anotherFloat.floatValue();
ensures \result < 0;
also
requires this.theFloat == anotherFloat.floatValue();
ensures \result == 0;
also
requires this.theFloat > anotherFloat.floatValue();
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.Float);
ensures \result == this.compareTo((java.lang.Float)o);
     also
public exceptional_behavior
requires o == null||!(o instanceof java.lang.Float);
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(float f1,
                          float f2)
Specifications: pure
public normal_behavior
assignable \nothing;
ensures \result == new java.lang.Float(f1).compareTo(new java.lang.Float(f2));

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.