JML

java.lang
Class Math

java.lang.Object
  extended byjava.lang.Math

public final strictfp class Math
extends Object

JML's specification of java.lang.Math.

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

Class Specifications
static public initially java.lang.Math.firstTimeCalledRandom;

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Model Field Summary
static boolean firstTimeCalledRandom
           
 
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 double E
           
static double PI
           
 
Constructor Summary
private Math()
           
 
Model Method Summary
static boolean close(double a, double b, double eps)
           
static boolean close(double a, double b, double c, double eps)
           
static boolean isFiniteEven(double a)
           
static boolean isFiniteOdd(double a)
           
static boolean isNegativeZero(double a)
           
static boolean isNegativeZero(float a)
           
static boolean isPositiveZero(double a)
           
static boolean isPositiveZero(float a)
           
 
Model methods inherited from class java.lang.Object
hashValue
 
Method Summary
static double abs(double a)
           
static float abs(float a)
           
static int abs(int a)
           
static long abs(long a)
           
static double acos(double a)
           
static double asin(double a)
           
static double atan(double a)
           
static double atan2(double y, double x)
           
static double ceil(double a)
           
static double cos(double a)
           
static double exp(double a)
           
static double floor(double a)
           
static double IEEEremainder(double f1, double f2)
           
static double log(double a)
           
static double max(double a, double b)
           
static float max(float a, float b)
           
static int max(int a, int b)
           
static long max(long a, long b)
           
static double min(double a, double b)
           
static float min(float a, float b)
           
static int min(int a, int b)
           
static long min(long a, long b)
           
static double pow(double a, double b)
           
static double random()
           
static double rint(double a)
           
static long round(double a)
           
static int round(float a)
           
static double sin(double a)
           
static double sqrt(double a)
           
static double tan(double a)
           
static double toDegrees(double angrad)
           
static double toRadians(double angdeg)
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Model Field Detail

firstTimeCalledRandom

public static boolean firstTimeCalledRandom
Field Detail

E

public static final double E

PI

public static final double PI
Constructor Detail

Math

private Math()
Specifications: (class)pure
Model Method Detail

isPositiveZero

public static boolean isPositiveZero(double a)
Specifications: pure

isNegativeZero

public static boolean isNegativeZero(double a)
Specifications: pure

isPositiveZero

public static boolean isPositiveZero(float a)
Specifications: pure

isNegativeZero

public static boolean isNegativeZero(float a)
Specifications: pure

isFiniteOdd

public static boolean isFiniteOdd(double a)
Specifications: pure

isFiniteEven

public static boolean isFiniteEven(double a)
Specifications: pure

close

public static boolean close(double a,
                            double b,
                            double eps)
Specifications: pure

close

public static boolean close(double a,
                            double b,
                            double c,
                            double eps)
Specifications: pure
Method Detail

sin

public static double sin(double a)
Specifications: pure
public normal_behavior
{|
requires java.lang.Double.isNaN(a)||java.lang.Double.isInfinite(a);
ensures java.lang.Double.isNaN(\result );
also
requires a == 0.0;
ensures \result == 0.0;
also
requires isPositiveZero(a);
ensures isPositiveZero(\result );
also
requires isNegativeZero(a);
ensures isNegativeZero(\result );
also
ensures !java.lang.Double.isNaN(\result ) ==> \result == java.lang.StrictMath.sin(a);
also
ensures (* result within 1 ulp of correctly rounded result *);
|}

cos

public static double cos(double a)
Specifications: pure
public normal_behavior
{|
requires java.lang.Double.isNaN(a)||java.lang.Double.isInfinite(a);
ensures java.lang.Double.isNaN(\result );
also
requires a == 0.0;
ensures \result == 1.0;
also
ensures !java.lang.Double.isNaN(\result ) ==> \result == java.lang.StrictMath.cos(a);
also
ensures (* result within 1 ulp of correctly rounded result *);
|}

tan

public static double tan(double a)
Specifications: pure
public normal_behavior
{|
requires java.lang.Double.isNaN(a)||java.lang.Double.isInfinite(a);
ensures java.lang.Double.isNaN(\result );
also
requires a == 0.0;
ensures \result == 0.0;
also
requires isPositiveZero(a);
ensures isPositiveZero(\result );
also
requires isNegativeZero(a);
ensures isNegativeZero(\result );
also
ensures !java.lang.Double.isNaN(\result ) ==> \result == java.lang.StrictMath.tan(a);
also
ensures (* result within 1 ulp of correctly rounded result *);
|}

asin

public static double asin(double a)
Specifications: pure
public normal_behavior
{|
requires java.lang.Double.isNaN(a)||abs(a) > 1.0;
ensures java.lang.Double.isNaN(\result );
also
requires a == 0.0;
ensures \result == 0.0;
also
requires isPositiveZero(a);
ensures isPositiveZero(\result );
also
requires isNegativeZero(a);
ensures isNegativeZero(\result );
also
requires !java.lang.Double.isNaN(a)&&abs(a) <= 1.0;
ensures sin(asin(a)) == a;
also
ensures !java.lang.Double.isNaN(\result ) ==> \result == java.lang.StrictMath.asin(a);
also
ensures (* result within 1 ulp of correctly rounded result *);
|}

acos

public static double acos(double a)
Specifications: pure
public normal_behavior
{|
requires java.lang.Double.isNaN(a)||abs(a) > 1.0;
ensures java.lang.Double.isNaN(\result );
also
requires !java.lang.Double.isNaN(a)&&abs(a) <= 1.0;
ensures close(cos(acos(a)),a,acos(a),1.0E-17);
also
ensures !java.lang.Double.isNaN(\result ) ==> \result == java.lang.StrictMath.acos(a);
also
ensures (* result within 1 ulp of correctly rounded result *);
|}

atan

public static double atan(double a)
Specifications: pure
public normal_behavior
{|
requires java.lang.Double.isNaN(a);
ensures java.lang.Double.isNaN(\result );
also
requires a == 0.0;
ensures \result == 0.0;
also
requires isPositiveZero(a);
ensures isPositiveZero(\result );
also
requires isNegativeZero(a);
ensures isNegativeZero(\result );
also
requires !java.lang.Double.isNaN(a)&&!java.lang.Double.isInfinite(a);
requires abs(a) < 1.0E16;
ensures close(tan(atan(a)),a,atan(a),1.0E-15);
also
ensures !java.lang.Double.isNaN(\result ) ==> \result == java.lang.StrictMath.atan(a);
also
ensures (* result within 1 ulp of correctly rounded result *);
|}

toRadians

public static double toRadians(double angdeg)
Specifications: pure
public normal_behavior
requires !java.lang.Double.isNaN(angdeg);
ensures \result == angdeg/180.0*3.141592653589793;
     also
public normal_behavior
requires java.lang.Double.isNaN(angdeg);
ensures java.lang.Double.isNaN(\result );

toDegrees

public static double toDegrees(double angrad)
Specifications: pure
public normal_behavior
requires !java.lang.Double.isNaN(angrad);
ensures \result == angrad*180.0/3.141592653589793;
     also
public normal_behavior
requires java.lang.Double.isNaN(angrad);
ensures java.lang.Double.isNaN(\result );

exp

public static double exp(double a)
Specifications: pure
public normal_behavior
{|
requires java.lang.Double.isNaN(a);
ensures java.lang.Double.isNaN(\result );
also
requires a == Infinity;
ensures \result == Infinity;
also
requires a == -Infinity;
ensures isPositiveZero(\result );
also
ensures !java.lang.Double.isNaN(\result ) ==> \result == java.lang.StrictMath.exp(a);
also
ensures (* result within 1 ulp of correctly rounded result *);
|}

log

public static double log(double a)
Specifications: pure
public normal_behavior
{|
requires java.lang.Double.isNaN(a)||a < 0.0;
ensures java.lang.Double.isNaN(\result );
also
requires a == Infinity;
ensures \result == Infinity;
also
requires a == 0.0;
ensures \result == -Infinity;
also
ensures !java.lang.Double.isNaN(\result ) ==> \result == java.lang.StrictMath.log(a);
also
ensures (* result within 1 ulp of correctly rounded result *);
|}

sqrt

public static double sqrt(double a)
Specifications: pure
public normal_behavior
{|
requires java.lang.Double.isNaN(a)||a < 0.0;
ensures java.lang.Double.isNaN(\result );
also
requires a == Infinity;
ensures \result == Infinity;
also
requires isPositiveZero(a);
ensures isPositiveZero(\result );
also
requires isNegativeZero(a);
ensures isNegativeZero(\result );
also
requires a > 0.0&&a < Infinity;
ensures close(a,sqrt(a)*sqrt(a),1.0E-17);
also
ensures !java.lang.Double.isNaN(\result ) ==> \result == java.lang.StrictMath.sqrt(a);
|}

IEEEremainder

public static double IEEEremainder(double f1,
                                   double f2)
Specifications: pure
public normal_behavior
{|
requires java.lang.Double.isNaN(f1)||java.lang.Double.isNaN(f2);
ensures java.lang.Double.isNaN(\result );
also
requires !java.lang.Double.isNaN(f1)&&!java.lang.Double.isNaN(f2);
{|
requires java.lang.Double.isInfinite(f1)||f2 == 0.0;
ensures java.lang.Double.isNaN(\result );
also
requires !java.lang.Double.isInfinite(f1)&&java.lang.Double.isInfinite(f2);
ensures \result == f1;
also
requires f1 == 1.7976931348623157E308&&f2 == 4.9E-324;
ensures \result == 0.0;
also
requires f2 != 0.0&&!java.lang.Double.isInfinite(f2)&&!java.lang.Double.isInfinite(f1/f2)&&!java.lang.Double.isInfinite(f2*rint(f1/f2))&&((f1/f2) != 0.0);
|}
|}

ceil

public static double ceil(double a)
Specifications: pure
public normal_behavior
{|
requires java.lang.Double.isNaN(a);
ensures java.lang.Double.isNaN(\result );
also
requires java.lang.Double.isInfinite(a)||a == 0.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 -1.7976931348623157E308 < a&&a < 1.7976931348623157E308;
ensures \result == rint(\result );
ensures a <= \result ;
ensures ((a+1.0) != 1.0) ==> \result < (a+1.0);
also
ensures !java.lang.Double.isNaN(\result ) ==> \result == java.lang.StrictMath.ceil(a);
|}

floor

public static double floor(double a)
Specifications: pure
public normal_behavior
{|
requires java.lang.Double.isInfinite(a)||a == 0.0;
ensures \result == a;
also
requires isPositiveZero(a);
ensures isPositiveZero(\result );
also
requires isNegativeZero(a);
ensures isNegativeZero(\result );
also
requires java.lang.Double.isNaN(a);
ensures java.lang.Double.isNaN(\result );
also
requires a == rint(a);
ensures \result == a;
also
requires -1.7976931348623157E308 < a&&a < 1.7976931348623157E308;
ensures \result == rint(\result );
ensures \result <= a;
ensures ((a-1.0) != -1.0) ==> (a-1.0) < \result ;
also
ensures !java.lang.Double.isNaN(\result ) ==> \result == java.lang.StrictMath.floor(a);
|}

rint

public static double rint(double a)
Specifications: pure
public normal_behavior
{|
requires !java.lang.Double.isNaN(a)&&!java.lang.Double.isInfinite(a)&&a != 0.0;
ensures (* \result is mathematical integer closest to a *);
also
requires isPositiveZero(a);
ensures isPositiveZero(\result );
also
requires isNegativeZero(a);
ensures isNegativeZero(\result );
also
requires java.lang.Double.isNaN(a);
ensures java.lang.Double.isNaN(\result );
also
requires java.lang.Double.isInfinite(a)||a == 0.0;
ensures \result == a;
|}

atan2

public static double atan2(double y,
                           double x)
Specifications: pure
public normal_behavior
{|
requires java.lang.Double.isNaN(y)||java.lang.Double.isNaN(x);
ensures java.lang.Double.isNaN(\result );
also
requires (isPositiveZero(y)&&x > 0.0)||(0.0 < y&&y < Infinity&&x == Infinity);
ensures isPositiveZero(\result );
also
requires (isNegativeZero(y)&&x > 0.0)||(-Infinity < y&&y < 0.0&&x == Infinity);
ensures isNegativeZero(\result );
also
requires (isPositiveZero(y)&&x < 0.0)||(0.0 < y&&y < Infinity&&x == -Infinity);
ensures \result == 3.141592653589793;
also
requires (isNegativeZero(y)&&x < 0.0)||(-Infinity < y&&y < 0.0&&x == -Infinity);
ensures \result == -3.141592653589793;
also
requires (y > 0.0&&x == 0.0)||(y == Infinity&&-Infinity < x&&x < Infinity);
ensures \result == 1.5707963267948966;
also
requires (y < 0.0&&x == 0.0)||(y == -Infinity&&-Infinity < x&&x < Infinity);
ensures \result == -1.5707963267948966;
also
requires y == x&&y > 0.0;
ensures \result == 0.7853981633974483;
also
requires y == -x&&y > 0.0;
ensures \result == 2.356194490192345;
also
requires y == -x&&y < 0.0;
ensures \result == -0.7853981633974483;
also
requires y == x&&y < 0.0;
ensures \result == -2.356194490192345;
also
ensures (* result within 2 ulp of correctly rounded result *);
|}

pow

public static double pow(double a,
                         double b)
Specifications: pure
public normal_behavior
{|
requires java.lang.Double.isNaN(b);
ensures java.lang.Double.isNaN(\result );
also
requires !java.lang.Double.isNaN(b);
{|
requires b == 0.0;
ensures \result == 1.0;
also
requires b == 1.0&&!java.lang.Double.isNaN(a);
ensures \result == a;
also
requires java.lang.Double.isNaN(a)&&b != 0.0;
ensures java.lang.Double.isNaN(\result );
also
requires (abs(a) > 1.0&&b == Infinity)||(abs(a) < 1.0&&b == -Infinity);
ensures \result == Infinity;
also
requires (abs(a) < 1.0&&b == Infinity)||(abs(a) > 1.0&&b == -Infinity);
ensures isPositiveZero(\result );
also
requires (a == -1.0||a == 1.0)&&java.lang.Double.isInfinite(b);
ensures java.lang.Double.isNaN(\result );
also
requires (isPositiveZero(a)&&b > 0.0)||(a == Infinity&&b < 0.0);
ensures isPositiveZero(\result );
also
requires (isPositiveZero(a)&&b < 0.0)||(a == Infinity&&b > 0.0);
ensures \result == Infinity;
also
requires (isNegativeZero(a)&&b > 0.0&&!isFiniteOdd(b))||(a == -Infinity&&b < 0.0&&!isFiniteOdd(b));
ensures isPositiveZero(\result );
also
requires (isNegativeZero(a)&&b > 0.0&&isFiniteOdd(b))||(a == -Infinity&&b < 0.0&&isFiniteOdd(b));
ensures isNegativeZero(\result );
also
requires (isNegativeZero(a)&&b < 0.0&&!isFiniteOdd(b))||(a == -Infinity&&b > 0.0&&!isFiniteOdd(b));
ensures \result == Infinity;
also
requires (isNegativeZero(a)&&b < 0.0&&isFiniteOdd(b))||(a == -Infinity&&b > 0.0&&isFiniteOdd(b));
ensures \result == -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 !java.lang.Double.isInfinite(a)&&a < 0.0&&!java.lang.Double.isInfinite(b)&&rint(b) != b;
ensures java.lang.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 *);
|}
|}

round

public static int round(float a)
Specifications: pure
public normal_behavior
{|
requires java.lang.Float.isNaN(a);
ensures \result == 0;
also
requires a == -Infinity||a <= -2.14748365E9;
ensures \result == -2147483648;
also
requires a == Infinity||a >= 2.14748365E9;
ensures \result == 2147483647;
also
requires !java.lang.Float.isNaN(a)&&!java.lang.Float.isInfinite(a)&&-2.14748365E9 < a&&a < 2.14748365E9;
ensures \result == (int)java.lang.Math.floor(a+0.5);
|}

round

public static long round(double a)
Specifications: pure
public normal_behavior
{|
requires java.lang.Double.isNaN(a);
ensures \result == 0;
also
requires a == -Infinity||a <= -9.223372036854776E18;
ensures \result == -9223372036854775808;
also
requires a == Infinity||a >= 9.223372036854776E18;
ensures \result == 9223372036854775807;
also
requires !java.lang.Double.isNaN(a)&&!java.lang.Double.isInfinite(a)&&-9.223372036854776E18 < a&&a < 9.223372036854776E18;
ensures \result == (long)java.lang.Math.floor(a+0.5);
|}

random

public static double random()
Specifications: (class)pure

abs

public static int abs(int a)
Specifications: pure
public normal_behavior
{|
requires a == -2147483648;
ensures \result == -2147483648;
also
requires a >= 0;
ensures \result == a;
also
requires a < 0;
ensures \result == -a;
|}
     also
public normal_behavior
ensures (\result != -2147483648) ==> \result >= 0;

abs

public static long abs(long a)
Specifications: pure
public normal_behavior
{|
requires a == -9223372036854775808;
ensures \result == -9223372036854775808;
also
requires a >= 0;
ensures \result == a;
also
requires a < 0;
ensures \result == -a;
|}
     also
public normal_behavior
ensures (\result != -9223372036854775808) ==> \result >= 0;

abs

public static float abs(float a)
Specifications: pure
public normal_behavior
{|
requires java.lang.Float.isNaN(a);
ensures java.lang.Float.isNaN(\result );
also
requires a == 0.0;
ensures isPositiveZero(\result );
also
requires java.lang.Float.isInfinite(a);
ensures \result == Infinity;
also
requires a > 0.0;
ensures \result == a;
also
requires a < 0.0;
ensures \result == -a;
|}
    implies_that
ensures !java.lang.Float.isNaN(a) ==> \result >= 0.0;

abs

public static double abs(double a)
Specifications: pure
public normal_behavior
{|
requires java.lang.Double.isNaN(a);
ensures java.lang.Double.isNaN(\result );
also
requires a == 0.0;
ensures isPositiveZero(\result );
also
requires java.lang.Double.isInfinite(a);
ensures \result == Infinity;
also
requires a > 0.0;
ensures \result == a;
also
requires a < 0.0;
ensures \result == -a;
|}
    implies_that
ensures !java.lang.Double.isNaN(a) ==> \result >= 0.0;

max

public static int max(int a,
                      int b)
Specifications: pure
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;

max

public static long max(long a,
                       long b)
Specifications: pure
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;

max

public static float max(float a,
                        float b)
Specifications: pure
public normal_behavior
{|
requires java.lang.Float.isNaN(a)||java.lang.Float.isNaN(b);
ensures java.lang.Float.isNaN(\result );
also
requires !(java.lang.Float.isNaN(a)||java.lang.Float.isNaN(b));
{|
requires (isPositiveZero(a)&&b == 0.0)||(isPositiveZero(b)&&a == 0.0);
ensures isPositiveZero(\result );
also
requires new java.lang.Float(a).compareTo(new java.lang.Float(b)) == 0;
ensures \result == a;
also
requires new java.lang.Float(a).compareTo(new java.lang.Float(b)) <= 0;
ensures \result == b;
also
requires new java.lang.Float(a).compareTo(new java.lang.Float(b)) >= 0;
ensures \result == a;
|}
|}

max

public static double max(double a,
                         double b)
Specifications: pure
public normal_behavior
{|
requires java.lang.Double.isNaN(a)||java.lang.Double.isNaN(b);
ensures java.lang.Double.isNaN(\result );
also
requires !(java.lang.Double.isNaN(a)||java.lang.Double.isNaN(b));
{|
requires (isPositiveZero(a)&&b == 0.0)||(isPositiveZero(b)&&a == 0.0);
ensures isPositiveZero(\result );
also
requires new java.lang.Double(a).compareTo(new java.lang.Double(b)) == 0;
ensures \result == a;
also
requires new java.lang.Double(a).compareTo(new java.lang.Double(b)) <= 0;
ensures \result == b;
also
requires new java.lang.Double(a).compareTo(new java.lang.Double(b)) >= 0;
ensures \result == a;
|}
|}

min

public static int min(int a,
                      int b)
Specifications: pure
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;

min

public static long min(long a,
                       long b)
Specifications: pure
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;

min

public static float min(float a,
                        float b)
Specifications: pure
public normal_behavior
{|
requires java.lang.Float.isNaN(a)||java.lang.Float.isNaN(b);
ensures java.lang.Float.isNaN(\result );
also
requires !(java.lang.Float.isNaN(a)||java.lang.Float.isNaN(b));
{|
requires (isNegativeZero(a)&&b == 0.0)||(isNegativeZero(b)&&a == 0.0);
ensures isNegativeZero(\result );
also
requires new java.lang.Float(a).compareTo(new java.lang.Float(b)) == 0;
ensures \result == a;
also
requires new java.lang.Float(a).compareTo(new java.lang.Float(b)) <= 0;
ensures \result == a;
also
requires new java.lang.Float(a).compareTo(new java.lang.Float(b)) >= 0;
ensures \result == b;
|}
|}

min

public static double min(double a,
                         double b)
Specifications: pure
public normal_behavior
{|
requires java.lang.Double.isNaN(a)||java.lang.Double.isNaN(b);
ensures java.lang.Double.isNaN(\result );
also
requires !(java.lang.Double.isNaN(a)||java.lang.Double.isNaN(b));
{|
requires (isNegativeZero(a)&&b == 0.0)||(isNegativeZero(b)&&a == 0.0);
ensures isNegativeZero(\result );
also
requires new java.lang.Double(a).compareTo(new java.lang.Double(b)) == 0;
ensures \result == a;
also
requires new java.lang.Double(a).compareTo(new java.lang.Double(b)) <= 0;
ensures \result == a;
also
requires new java.lang.Double(a).compareTo(new java.lang.Double(b)) >= 0;
ensures \result == b;
|}
|}

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.