// @(#)$Id: Math.jml,v 1.22 2005/07/07 21:03:10 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; import java.util.Random; /** JML's specification of java.lang.Math. * @version $Revision: 1.22 $ * @author Brandon Shilling * @author David Cok * @author Gary T. Leavens */ /* CAUTION: Note that - there is a difference between positive and negative 0 - primitive == does not distinguish between positive and negative zero that is, (+0.0 == -0.0) is true; use isPositiveZero and isNegativeZero when you need to distinguish these - NaN compares false to everything: (NaN == NaN) is false; you have to use Double.isNaN(\...) - primitive == is not the same as .equals on Doubles - primitive comparisions (<, >, <=, >=) on doubles are not the same as .comparesTo on Doubles */ public /*@ pure @*/ final strictfp class Math { /*@ public static model boolean firstTimeCalledRandom; @ public static initially firstTimeCalledRandom; @*/ private Math(); public static final double E; public static final double PI; /*@ public normal_behavior @ {| @ requires Double.isNaN(a) || Double.isInfinite(a); @ ensures Double.isNaN(\result); @ also @ requires a == 0; // positive or negative zero @ ensures \result == 0; @ also @ requires isPositiveZero(a); @ ensures isPositiveZero(\result); @ also @ requires isNegativeZero(a); @ ensures isNegativeZero(\result); @ also @ ensures !Double.isNaN(\result) ==> \result == StrictMath.sin(a); @ also @ ensures (* result within 1 ulp of correctly rounded result *); @ |} @*/ public static /*@ pure @*/ double sin(double a); /*@ public normal_behavior @ {| @ requires Double.isNaN(a) || Double.isInfinite(a); @ ensures Double.isNaN(\result); @ also @ requires a == 0; // positive or negative zero @ ensures \result == 1.0; @ also @ ensures !Double.isNaN(\result) ==> \result == StrictMath.cos(a); @ also @ ensures (* result within 1 ulp of correctly rounded result *); @ |} @*/ public static /*@ pure @*/ double cos(double a); /*@ public normal_behavior @ {| @ requires Double.isNaN(a) || Double.isInfinite(a); @ ensures Double.isNaN(\result); @ also @ requires a == 0; // positive or negative zero @ ensures \result == 0; @ also @ requires isPositiveZero(a); @ ensures isPositiveZero(\result); @ also @ requires isNegativeZero(a); @ ensures isNegativeZero(\result); @ also @ ensures !Double.isNaN(\result) ==> \result == StrictMath.tan(a); @ also @ ensures (* result within 1 ulp of correctly rounded result *); @ |} @*/ public static /*@ pure @*/ double tan(double a); /*@ public normal_behavior @ {| @ requires Double.isNaN(a) || abs(a) > 1; @ ensures Double.isNaN(\result); @ also @ requires a == 0; // positive or negative zero @ ensures \result == 0; @ also @ requires isPositiveZero(a); @ ensures isPositiveZero(\result); @ also @ requires isNegativeZero(a); @ ensures isNegativeZero(\result); @ also @ requires !Double.isNaN(a) && abs(a) <= 1; @ ensures sin(asin(a)) == a; @ also @ ensures !Double.isNaN(\result) ==> \result == StrictMath.asin(a); @ also @ ensures (* result within 1 ulp of correctly rounded result *); @ |} @*/ public static /*@ pure @*/ double asin(double a); /*@ public normal_behavior @ {| @ requires Double.isNaN(a) || abs(a) > 1; @ ensures Double.isNaN(\result); @ also @ requires !Double.isNaN(a) && abs(a) <= 1; @ ensures close(cos(acos(a)),a,acos(a),1.e-17); @ also @ ensures !Double.isNaN(\result) ==> \result == StrictMath.acos(a); @ also @ ensures (* result within 1 ulp of correctly rounded result *); @ |} @*/ public static /*@ pure @*/ double acos(double a); /*@ public normal_behavior @ {| @ requires Double.isNaN(a); @ ensures Double.isNaN(\result); @ also @ requires a == 0; // positive or negative zero @ ensures \result == 0; @ also @ requires isPositiveZero(a); @ ensures isPositiveZero(\result); @ also @ requires isNegativeZero(a); @ ensures isNegativeZero(\result); @ also @ requires !Double.isNaN(a) && !Double.isInfinite(a); @ requires abs(a) < 1.e16; // FIXME - to avoid precision problems @ ensures close(tan(atan(a)),a,atan(a),1e-15); @ also @ ensures !Double.isNaN(\result) ==> \result == StrictMath.atan(a); @ also @ ensures (* result within 1 ulp of correctly rounded result *); @ |} @*/ public static /*@ pure @*/ double atan(double a); /*@ public normal_behavior @ requires !Double.isNaN(angdeg); @ ensures \result == angdeg / 180.0 * PI; @ also @ public normal_behavior @ requires Double.isNaN(angdeg); @ ensures Double.isNaN(\result); @*/ public static /*@ pure @*/ double toRadians(double angdeg); /*@ public normal_behavior @ requires !Double.isNaN(angrad); @ ensures \result == angrad * 180.0 / PI; @ also @ public normal_behavior @ requires Double.isNaN(angrad); @ ensures Double.isNaN(\result); @*/ public static /*@ pure @*/ double toDegrees(double angrad); /*@ public normal_behavior @ {| @ requires Double.isNaN(a); @ ensures Double.isNaN(\result); @ also @ requires a == Double.POSITIVE_INFINITY; @ ensures \result == Double.POSITIVE_INFINITY; @ also @ requires a == Double.NEGATIVE_INFINITY; @ ensures isPositiveZero(\result); @ also @ ensures !Double.isNaN(\result) ==> \result == StrictMath.exp(a); @ also @ ensures (* result within 1 ulp of correctly rounded result *); @ |} @*/ public static /*@ pure @*/ double exp(double a); /*@ public normal_behavior @ {| @ requires Double.isNaN(a) || a < 0.0; @ ensures Double.isNaN(\result); @ also @ requires a == Double.POSITIVE_INFINITY; @ ensures \result == Double.POSITIVE_INFINITY; @ also @ requires a == 0; // positive or negative zero @ ensures \result == Double.NEGATIVE_INFINITY; @ also @ ensures !Double.isNaN(\result) ==> \result == StrictMath.log(a); @ also @ ensures (* result within 1 ulp of correctly rounded result *); @ |} @*/ public static /*@ pure @*/ double log(double a); /*@ public normal_behavior @ {| @ requires Double.isNaN(a) || a < 0.0; @ ensures Double.isNaN(\result); @ also @ requires a == Double.POSITIVE_INFINITY; @ ensures \result == Double.POSITIVE_INFINITY; @ also @ requires isPositiveZero(a); @ ensures isPositiveZero(\result); @ also @ requires isNegativeZero(a); @ ensures isNegativeZero(\result); @ also @ requires a > 0 && a < Double.POSITIVE_INFINITY; @ // ensures a == sqrt(a) * sqrt(a); @ ensures close(a,sqrt(a)*sqrt(a),1.e-17); @ also @ ensures !Double.isNaN(\result) ==> \result == StrictMath.sqrt(a); @ |} @*/ public static /*@ pure @*/ double sqrt(double a); /*@ public normal_behavior @ {| @ requires Double.isNaN(f1) || Double.isNaN(f2); @ ensures Double.isNaN(\result); @ also @ requires !Double.isNaN(f1) && !Double.isNaN(f2); @ {| @ requires Double.isInfinite(f1) || f2 == 0.0; @ ensures Double.isNaN(\result); @ also @ requires !Double.isInfinite(f1) && Double.isInfinite(f2); @ ensures \result == f1; @ also @ requires f1 == Double.MAX_VALUE && f2 == Double.MIN_VALUE; @ ensures \result == 0; @ also @ requires f2 != 0 @ && !Double.isInfinite(f2) @ && !Double.isInfinite(f1/f2) @ && !Double.isInfinite(f2 * rint(f1/f2)) @ && ((f1/f2) != 0) ; @ // FIXME - need a postcondition that works when precision is lost, // e.g. for when f1 is MAX_VALUE @ //ensures \result == f1 - f2 * rint(f1 / f2 ); @ //ensures \result == f2 * ( (f1/f2) - rint(f1 / f2 ) ); @ |} @ |} @*/ public static /*@ pure @*/ double IEEEremainder(double f1, double f2); /*@ public normal_behavior @ {| @ requires Double.isNaN(a); @ ensures Double.isNaN(\result); @ also @ requires Double.isInfinite(a) || a == 0; // positive or negative 0 @ ensures \result == a; @ also @ requires isPositiveZero(a); @ ensures isPositiveZero(\result); @ also @ requires isNegativeZero(a); @ ensures isNegativeZero(\result); @ also @ requires -1.0 < a && a < 0.0; @ ensures isNegativeZero(\result); @ also @ requires a == rint(a); @ ensures \result == a; @ also @ requires -Double.MAX_VALUE < a && a < Double.MAX_VALUE; @ ensures \result == rint(\result); @ ensures a <= \result; @ ensures ((a+1) != 1) ==> \result < (a+1); // Guard is for precision problems @ also @ ensures !Double.isNaN(\result) ==> \result == StrictMath.ceil(a); @ |} @*/ public static /*@ pure @*/ double ceil(double a); /*@ public normal_behavior @ {| @ requires Double.isInfinite(a) || a == 0; // positive or negative 0 @ ensures \result == a; @ also @ requires isPositiveZero(a); @ ensures isPositiveZero(\result); @ also @ requires isNegativeZero(a); @ ensures isNegativeZero(\result); @ also @ requires Double.isNaN(a); @ ensures Double.isNaN(\result); @ also @ requires a == rint(a); @ ensures \result == a; @ also @ requires -Double.MAX_VALUE < a && a < Double.MAX_VALUE; @ ensures \result == rint(\result); @ ensures \result <= a; @ ensures ((a-1) != -1) ==> (a-1) < \result; // Guard is for precision problems @ also @ ensures !Double.isNaN(\result) ==> \result == StrictMath.floor(a); @ |} @*/ public static /*@ pure @*/ double floor(double a); /*@ public normal_behavior @ {| @ requires !Double.isNaN(a) && !Double.isInfinite(a) @ && a != 0; @ ensures (* \result is mathematical integer closest to a *); // FIXME @ also @ requires isPositiveZero(a); @ ensures isPositiveZero(\result); @ also @ requires isNegativeZero(a); @ ensures isNegativeZero(\result); @ also @ requires Double.isNaN(a); @ ensures Double.isNaN(\result); @ also @ requires Double.isInfinite(a) || a == 0.0; // pos or neg zero @ ensures \result == a; @ |} @*/ public static /*@ pure @*/ double rint(double a); /*@ public normal_behavior @ {| @ requires Double.isNaN(y) || Double.isNaN(x); @ ensures Double.isNaN(\result); @ also @ requires (isPositiveZero(y) && x > 0.0) @ || (0 < y && y 0.0) @ || (Double.NEGATIVE_INFINITY < y && y < 0 @ && x ==Double.POSITIVE_INFINITY); @ ensures isNegativeZero(\result); @ also @ requires (isPositiveZero(y) && x < 0.0) @ || (0 < y && y 0.0 && x == 0) @ || ( y ==Double.POSITIVE_INFINITY @ && Double.NEGATIVE_INFINITY < x @ && x 0; @ ensures \result == PI/4; @ also @ requires y == -x && y > 0; @ ensures \result == (3*PI)/4; @ also @ requires y == -x && y < 0; @ ensures \result == -(PI)/4; @ also @ requires y == x && y < 0; @ ensures \result == -(3*PI)/4; @ also @ ensures (* result within 2 ulp of correctly rounded result *); @ |} @*/ public static /*@ pure @*/ double atan2(double y, double x); /*@ public normal_behavior @ {| @ requires Double.isNaN(b); @ ensures Double.isNaN(\result); @ also @ requires !Double.isNaN(b); @ {| @ requires b == 0; // positive or negative zero @ ensures \result == 1.0; @ also @ requires b == 1.0 && !Double.isNaN(a); @ ensures \result == a; @ also @ requires Double.isNaN(a) && b != 0; // positive or negative 0 @ ensures Double.isNaN(\result); @ also @ requires (abs(a) > 1 && b == Double.POSITIVE_INFINITY) || @ (abs(a) < 1 && b == Double.NEGATIVE_INFINITY); @ ensures \result == Double.POSITIVE_INFINITY; @ also @ requires (abs(a) < 1 && b == Double.POSITIVE_INFINITY) || @ (abs(a) > 1 && b == Double.NEGATIVE_INFINITY); @ ensures isPositiveZero(\result); @ also @ requires (a == -1.0 || a == 1.0) && Double.isInfinite(b); @ ensures Double.isNaN(\result); @ also @ requires (isPositiveZero(a) && b > 0.0) @ || (a == Double.POSITIVE_INFINITY && b < 0.0); @ ensures isPositiveZero(\result); @ also @ requires (isPositiveZero(a) && b < 0.0) @ || (a == Double.POSITIVE_INFINITY && b > 0.0); @ ensures \result ==Double.POSITIVE_INFINITY; @ also @ requires (isNegativeZero(a) && b > 0.0 && !isFiniteOdd(b)) @ || (a == Double.NEGATIVE_INFINITY && b < 0.0 && !isFiniteOdd(b)); @ ensures isPositiveZero(\result); @ also @ requires (isNegativeZero(a) && b > 0.0 && isFiniteOdd(b)) @ || (a == Double.NEGATIVE_INFINITY && b < 0.0 && isFiniteOdd(b)); @ ensures isNegativeZero(\result); @ also @ requires (isNegativeZero(a) && b < 0.0 && !isFiniteOdd(b)) @ || (a == Double.NEGATIVE_INFINITY && b > 0.0 && !isFiniteOdd(b)); @ ensures \result ==Double.POSITIVE_INFINITY; @ also @ requires (isNegativeZero(a) && b < 0.0 && isFiniteOdd(b)) @ || (a == Double.NEGATIVE_INFINITY && b > 0.0 && isFiniteOdd(b)); @ ensures \result == Double.NEGATIVE_INFINITY; @ also @ requires (a < 0.0 && isFiniteOdd(b)); @ ensures \result == - pow(-a,b); @ also @ requires (a < 0.0 && isFiniteEven(b)); @ ensures \result == pow( -a, b); @ also @ requires !Double.isInfinite(a) && a < 0.0 && !Double.isInfinite(b) @ && rint(b) != b; @ ensures Double.isNaN(\result); @ also @ requires rint(a) == a && rint(b) == b; @ ensures (* \result is a raised to the power of b *) @ <==> (* \result can be represented as a double *); @ |} @ |} @*/ public static /*@ pure @*/ double pow(double a, double b); /*@ public normal_behavior @ {| @ requires Float.isNaN(a); @ ensures \result == 0; // NOTE THIS NON-INTUITIVE BEHAVIOR @ also @ requires a == Float.NEGATIVE_INFINITY || a <= Integer.MIN_VALUE; @ ensures \result == Integer.MIN_VALUE; @ also @ requires a == Float.POSITIVE_INFINITY || a >= Integer.MAX_VALUE; @ ensures \result == Integer.MAX_VALUE; @ also @ requires !Float.isNaN(a) && !Float.isInfinite(a) @ && Integer.MIN_VALUE < a && a < Integer.MAX_VALUE; @ ensures \result == (int)Math.floor(a + 0.5f); @ |} @*/ // rounds n+.5 to n+1 public static /*@ pure @*/ int round(float a); /*@ public normal_behavior @ {| @ requires Double.isNaN(a); @ ensures \result == 0; // NOTE THIS NON-INTUITIVE BEHAVIOR @ also @ requires a == Double.NEGATIVE_INFINITY || a <= Long.MIN_VALUE; @ ensures \result == Long.MIN_VALUE; @ also @ requires a == Double.POSITIVE_INFINITY || a >= Long.MAX_VALUE; @ ensures \result == Long.MAX_VALUE; @ also @ requires !Double.isNaN(a) && !Double.isInfinite(a) @ && Long.MIN_VALUE < a && a < Long.MAX_VALUE; @ ensures \result == (long)Math.floor(a + 0.5d); @ |} @*/ // rounds n+.5 to n+1 public static /*@ pure @*/ long round(double a); // FIXME - commented out because there is no implementation of firstTimeCalledRandom /* public normal_behavior @ {| @ requires firstTimeCalledRandom; @ assignable firstTimeCalledRandom; @ //ensures \result == StrictMath.random(); @ also @ requires !firstTimeCalledRandom; @ //ensures \result == StrictMath.random(); // FIXME - random is not pure; should have complained @ |} @*/ // FIXME - what is the range of the result? public static double random(); /*@ public normal_behavior @ {| @ requires a == Integer.MIN_VALUE; @ ensures \result == Integer.MIN_VALUE; @ also @ requires a >= 0; @ ensures \result == a; @ also @ requires a < 0; @ ensures \result == -a; @ |} @*/ //@ also public normal_behavior //@ ensures (\result != Integer.MIN_VALUE) ==> \result >= 0; public static /*@ pure @*/ int abs(int a); /*@ public normal_behavior @ {| @ requires a == Long.MIN_VALUE; @ ensures \result == Long.MIN_VALUE; @ also @ requires a >= 0; @ ensures \result == a; @ also @ requires a < 0; @ ensures \result == -a; @ |} @*/ //@ also public normal_behavior //@ ensures (\result != Long.MIN_VALUE) ==> \result >= 0L; public static /*@ pure @*/ long abs(long a); /*@ public normal_behavior @ {| @ requires Float.isNaN(a); @ ensures Float.isNaN(\result); @ also @ requires a == 0; // positive or negative 0 @ ensures isPositiveZero(\result); @ also @ requires Float.isInfinite(a); @ ensures \result == Float.POSITIVE_INFINITY; @ also @ requires a > 0; @ ensures \result == a; @ also @ requires a < 0; @ ensures \result == -a; @ |} @*/ //@ implies_that //@ ensures !Float.isNaN(a) ==> \result >= 0.0f; public static /*@ pure @*/ float abs(float a); /*@ public normal_behavior @ {| @ requires Double.isNaN(a); @ ensures Double.isNaN(\result); @ also @ requires a == 0; // positive or negative zero @ ensures isPositiveZero(\result); @ also @ requires Double.isInfinite(a); @ ensures \result == Double.POSITIVE_INFINITY; @ also @ requires a > 0; @ ensures \result == a; @ also @ requires a < 0; @ ensures \result == -a; @ |} @*/ //@ implies_that //@ ensures !Double.isNaN(a) ==> \result >= 0.0; public static /*@ pure @*/ double abs(double a); /*@ public normal_behavior @ {| @ requires a == b; @ ensures \result == a; @ also @ requires a <= b; @ ensures \result == b; @ also @ requires a >= b; @ ensures \result == a; @ |} @*/ //@ implies_that //@ ensures \result >= a && \result >= b; //@ ensures \result == a || \result == b; public static /*@ pure @*/ int max(int a, int b); /*@ public normal_behavior @ {| @ requires a == b; @ ensures \result == a; @ also @ requires a <= b; @ ensures \result == b; @ also @ requires a >= b; @ ensures \result == a; @ |} @*/ //@ implies_that //@ ensures \result >= a && \result >= b; //@ ensures \result == a || \result == b; public static /*@ pure @*/ long max(long a, long b); /*@ public normal_behavior @ {| @ requires Float.isNaN(a) || Float.isNaN(b); @ ensures Float.isNaN(\result); @ also @ requires !(Float.isNaN(a) || Float.isNaN(b)); @ {| @ requires (isPositiveZero(a) && b == 0) @ || (isPositiveZero(b) && a == 0); @ ensures isPositiveZero(\result); @ also @ requires new Float(a).compareTo(new Float(b)) == 0; @ ensures \result == a; @ also @ requires new Float(a).compareTo(new Float(b)) <= 0; @ ensures \result == b; @ also @ requires new Float(a).compareTo(new Float(b)) >= 0; @ ensures \result == a; @ |} @ |} @*/ public static /*@ pure @*/ float max(float a, float b); /*@ public normal_behavior @ {| @ requires Double.isNaN(a) || Double.isNaN(b); @ ensures Double.isNaN(\result); @ also @ requires !( Double.isNaN(a) || Double.isNaN(b)); @ {| @ requires (isPositiveZero(a) && b == 0) @ || (isPositiveZero(b) && a == 0); @ ensures isPositiveZero(\result); @ also @ requires new Double(a).compareTo(new Double(b)) == 0; @ ensures \result == a; @ also @ requires new Double(a).compareTo(new Double(b)) <= 0; @ ensures \result == b; @ also @ requires new Double(a).compareTo(new Double(b)) >= 0; @ ensures \result == a; @ |} @ |} @*/ public static /*@ pure @*/ double max(double a, double b); /*@ public normal_behavior @ {| @ requires a == b; @ ensures \result == a; @ also @ requires a >= b; @ ensures \result == b; @ also @ requires a <= b; @ ensures \result == a; @ |} @*/ //@ implies_that //@ ensures \result <= a && \result <= b; //@ ensures \result == a || \result == b; public static /*@ pure @*/ int min(int a, int b); /*@ public normal_behavior @ {| @ requires a == b; @ ensures \result == a; @ also @ requires a >= b; @ ensures \result == b; @ also @ requires a <= b; @ ensures \result == a; @ |} @*/ //@ implies_that //@ ensures \result <= a && \result <= b; //@ ensures \result == a || \result == b; public static /*@ pure @*/ long min(long a, long b); /*@ public normal_behavior @ {| @ requires Float.isNaN(a) || Float.isNaN(b); @ ensures Float.isNaN(\result); @ also @ requires !(Float.isNaN(a) || Float.isNaN(b)); @ {| @ requires (isNegativeZero(a) && b == 0) || (isNegativeZero(b) && a == 0); @ ensures isNegativeZero(\result); @ also @ requires new Float(a).compareTo(new Float(b)) == 0; @ ensures \result == a; @ also @ requires new Float(a).compareTo(new Float(b)) <= 0; @ ensures \result == a; @ also @ requires new Float(a).compareTo(new Float(b)) >= 0; @ ensures \result == b; @ |} @ |} @*/ public static /*@ pure @*/ float min(float a, float b); /*@ public normal_behavior @ {| @ requires Double.isNaN(a) || Double.isNaN(b); @ ensures Double.isNaN(\result); @ also @ requires !(Double.isNaN(a) || Double.isNaN(b)); @ {| @ requires (isNegativeZero(a) && b == 0) || (isNegativeZero(b) && a == 0); @ ensures isNegativeZero(\result); @ also @ requires new Double(a).compareTo(new Double(b)) == 0; @ ensures \result == a; @ also @ requires new Double(a).compareTo(new Double(b)) <= 0; @ ensures \result == a; @ also @ requires new Double(a).compareTo(new Double(b)) >= 0; @ ensures \result == b; @ |} @ |} @*/ public static /*@ pure @*/ double min(double a, double b); /*@ public static model pure boolean isPositiveZero( double a) { return new Double(a).equals(new Double("+0.0")); //return java.lang.Double.isPositiveZero(a); } public static model pure boolean isNegativeZero( double a) { return new Double(a).equals(new Double("-0.0")); //return java.lang.Double.isNegativeZero(a); } public static model pure boolean isPositiveZero( float a) { return new Float(a).equals(new Float("+0.0")); //return java.lang.Float.isPositiveZero(a); } public static model pure boolean isNegativeZero( float a) { return new Float(a).equals(new Float("-0.0")); //return java.lang.Float.isNegativeZero(a); } // FIXME - can't seem to reference model methods in other specs @*/ /*@ @ public static model pure boolean isFiniteOdd( double a ) { @ if( (a - 2*floor(a/2)) == 1.0 @ && Double.NEGATIVE_INFINITY < a && a