// @(#)$Id: Float.jml,v 1.19 2007/02/08 14:05:50 leavens Exp $ // // Copyright (C) 2005 Iowa State University // // This file is part of the runtime library of the Java Modeling Language. // // This library is free software; you can redistribute it and/or // modify it under the terms of the GNU Lesser General Public License // as published by the Free Software Foundation; either version 2.1, // of the License, or (at your option) any later version. // // This library is distributed in the hope that it will be useful, // but WITHOUT ANY WARRANTY; without even the implied warranty of // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU // Lesser General Public License for more details. // // You should have received a copy of the GNU Lesser General Public License // along with JML; see the file LesserGPL.txt. If not, write to the Free // Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA // 02110-1301 USA. package java.lang; /** JML's specification of java.lang.Float. * @version $Revision: 1.19 $ * @author Brandon Shilling * @author David R. Cok * @author Gary T. Leavens */ //-@ immutable public /*@ pure @*/ final class Float extends Number implements Comparable { //@ public model float theFloat; //@ public represents theFloat <- floatValue(); /** Returns true if the string is parseable as a float value (but not an infinite or NaN value). */ /*@ 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; @ |} @ public static model pure boolean parseable( String s ) { try { Float d = Float.valueOf(s); return true; } catch (Exception e) { return false; } } @*/ public static final float POSITIVE_INFINITY; public static final float NEGATIVE_INFINITY; public static final float NaN; public static final float MAX_VALUE; public static final float MIN_VALUE; /*@ 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 == Float.POSITIVE_INFINITY) ==>\result.equals("Infinity"); @ ensures (f == Float.NEGATIVE_INFINITY) ==>\result.equals("-Infinity"); @*/ // Note - I don't know of any parseable representation for // NaN or infinite values public static /*@ pure @*/ /*@ non_null @*/ String toString(float f); /*@ public normal_behavior @ requires s != null && parseable(s); @ ensures \result.equals(new Float(parseFloat(s))); @ also @ public exceptional_behavior @ requires s != null && !parseable(s); @ signals(NumberFormatException); @*/ public static /*@ pure @*/ /*@ non_null @*/ Float valueOf( /*@ non_null @*/ String s) throws NumberFormatException; /*@ public normal_behavior @ requires s != null && parseable(s); @ ensures true; // FIXME - put some conditions on the result @ also @ public exceptional_behavior @ requires s != null && !parseable(s); @ signals(NumberFormatException); @*/ public static /*@ pure @*/ float parseFloat(/*@ non_null @*/ String s) throws NumberFormatException; /*@ public normal_behavior @ ensures \result == !(v == v); @*/ public static /*@ pure @*/ boolean isNaN(float v); /*@ public normal_behavior @ ensures \result == ( v == POSITIVE_INFINITY @ || v == NEGATIVE_INFINITY ); @*/ public static /*@ pure @*/ boolean isInfinite(float v); /*@ public normal_behavior @ assignable theFloat; @ ensures identical(theFloat, value); @*/ public Float(float value); /*@ public normal_behavior @ assignable theFloat; @ ensures identical(theFloat, (float)value); @*/ public Float(double value); /*@ public normal_behavior @ requires parseable(s); @ assignable theFloat; @ ensures identical(theFloat, parseFloat(s)); @ also @ public exceptional_behavior @ requires !parseable(s); @ signals(NumberFormatException); @*/ public Float(String s) throws NumberFormatException; /*@ public normal_behavior @ requires true; @ ensures \result == !(theFloat == theFloat); @*/ public boolean isNaN(); /*@ public normal_behavior @ ensures \result == ( theFloat == POSITIVE_INFINITY @ || theFloat == NEGATIVE_INFINITY ); @*/ public boolean isInfinite(); // specification inherited from java.lang.Object //@ also ensures \result.equals(toString(floatValue())); public /*@ non_null @*/ String toString(); /*@ also @ public normal_behavior @ ensures \result == (byte) theFloat; @*/ public byte byteValue(); /*@ also @ public normal_behavior @ ensures \result == (short) theFloat; @*/ public short shortValue(); /*@ also @ public normal_behavior @ ensures \result == (int) theFloat; @*/ public int intValue(); /*@ also @ public normal_behavior @ ensures \result == (long) theFloat; @*/ public long longValue(); /*@ also @ public normal_behavior @ ensures identical(theFloat, \result); @*/ public float floatValue(); /*@ also @ public normal_behavior @ ensures Double.identical((double)theFloat, \result); @*/ public double doubleValue(); /*@ also @ public normal_behavior @ ensures (* \result is a hashcode value for this object *); @*/ public int hashCode(); /*@ also @ public normal_behavior @ requires obj != null && (obj instanceof Float); @ ensures \result == identical(theFloat, ((Float)obj).floatValue()); @ also public normal_behavior @ requires obj != null && !(obj instanceof Float); @ ensures !\result; @*/ public boolean equals(/*@ nullable @*/ Object obj); /*@ public normal_behavior @ {| @ requires value == POSITIVE_INFINITY; @ ensures \result == 0x7f800000; @ also @ requires value == NEGATIVE_INFINITY; @ ensures \result == 0xff800000; @ also @ requires new Float(value).isNaN(); @ ensures \result == 0x7fc00000; @ 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; @*/ public static /*@ pure @*/ native int floatToIntBits(float value); /*@ public normal_behavior @ {| @ requires value == POSITIVE_INFINITY; @ ensures \result == 0x7f800000; @ also @ requires value == NEGATIVE_INFINITY; @ ensures \result == 0xff800000; @ 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; @*/ public static /*@ pure @*/ native int floatToRawIntBits(float value); /*@ public normal_behavior @ {| @ requires bits == 0x7f800000; @ ensures \result == POSITIVE_INFINITY; @ also @ requires bits == 0xff800000; @ ensures \result == NEGATIVE_INFINITY; @ also @ requires ( 0x7f800001 <= bits && bits <= 0x7fffffff ) @ || ( 0xff800001 <= bits && bits <= 0xffffffff ); @ ensures new Float(\result).isNaN(); @ also @ ensures (* \result is floating-point value with @ the same bit pattern as bits *); @ |} @*/ public static /*@ pure @*/ native float intBitsToFloat(int bits); /*@ 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(theFloat) && @ isNegativeZero(anotherFloat.floatValue()); @ ensures \result > 0; @ also @ requires isNegativeZero(theFloat) && @ isPositiveZero(anotherFloat.floatValue()); @ ensures \result < 0; @ also @ requires !(this.isNaN() || anotherFloat.isNaN()) @ && !(isPositiveZero(theFloat) @ && isNegativeZero(anotherFloat.floatValue())) @ && !(isNegativeZero(theFloat) @ && isPositiveZero(anotherFloat.floatValue())); @ {| @ requires theFloat < anotherFloat.floatValue(); @ ensures \result < 0; @ also @ requires theFloat == anotherFloat.floatValue(); @ ensures \result == 0; @ also @ requires theFloat > anotherFloat.floatValue(); @ ensures \result > 0; @ |} @ |} @*/ public int compareTo(/*@ non_null @*/ Float anotherFloat); /*@ also @ public normal_behavior @ requires o != null && (o instanceof Float); @ ensures \result == compareTo((Float) o); @ also @ public exceptional_behavior @ requires o == null || !(o instanceof Float); @ signals(ClassCastException); @*/ public int compareTo(/*@ non_null @*/ Object o); /*@ public normal_behavior @ assignable \nothing; @ ensures \result == new Float(f1).compareTo(new Float(f2)); @*/ public static /*@ pure @*/ int compare(float f1, float f2); /** Returns true if the argument is a negative (and not positive) zero; the usual == returns true for comparing positive and negative zero. */ /*@ public static model pure boolean isNegativeZero( float a) { if (a != 0) return false; return (new java.lang.Float(a)).equals(new java.lang.Float("-0.0f")); } @*/ /** Returns true if the argument is a positive (and not negative) zero; the usual == returns true for comparing positive and negative zero. */ /*@ public static model pure boolean isPositiveZero( float a) { if (a != 0) return false; return (new java.lang.Float(a)).equals(new java.lang.Float("+0.0f")); } @*/ /** 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. */ /*@ public static model pure boolean identical(float a, float b) { return (isNaN(a) == isNaN(b)) && (isPositiveZero(a) == isPositiveZero(b)) && (isNegativeZero(a) == isNegativeZero(b)) && (isNaN(a) || isNaN(b) || (a==b)); } */ public static final /*@non_null@*/ Class TYPE; }