org.jmlspecs.models
Class JMLMath

java.lang.Object
  org.jmlspecs.models.JMLMath

public final strictfp class JMLMath

extends Object

A JML class that implements methods equivalent to those available in Math but that are defined over \bigint and \real instead.

Version:

$Revision: 1.5 $

Author:

Patrice Chalin

See Also:

Class Specifications

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Constructor Summary
private	JMLMath()           Don't let anyone instantiate this class.

 

Model Method Summary
static \bigint	abs(\bigint a)           Returns the absolute value of a \bigint value.
static \real	abs(\real a)           Returns the absolute value of a \real value.
static \real	ceil(\real a)           Returns the smallest (closest to negative infinity) \real value that is not less than the argument and is equal to a mathematical integer.
static \real	floor(\real a)           Returns the largest (closest to positive infinity) \real value that is not greater than the argument and is equal to a mathematical integer.
static \bigint	max(\bigint a, \bigint b)           Returns the greater of two \bigint values.
static \real	max(\real a, \real b)           Returns the greater of two \real values.
static \bigint	min(\bigint a, \bigint b)           Returns the smaller of two int values.
static \real	min(\real a, \real b)           Returns the smaller of two \real values.
static \bigint	nearestInteger(\real a)
static \real	pow(\real a, \real b)           Returns of value of the first argument raised to the power of the second argument.
static \real	rint(\real a)           Returns the \real value that is closest in value to the argument and is equal to a mathematical integer.
static \bigint	round(\real a)           Returns the closest \bigint to the argument.
static \real	sqrt(\real a)           The \real value that is closer than any other to e, the base of the natural logarithms. !

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Constructor Detail

JMLMath

private JMLMath()

Don't let anyone instantiate this class.

Specifications: (class)pure

sqrt

public static \real sqrt(\real a)

The \real value that is closer than any other to e, the base of the natural logarithms. !FIXME! define exactly. The \real value that is closer than any other to pi, the ratio of the circumference of a circle to its diameter. !FIXME! define exactly. Returns the correctly rounded positive square root of a \real value.

Parameters:

a - a value.

Returns:

the positive square root of a.

Specifications: pure

public normal_behavior
ensures \result > 0.0&&\result *\result == a;

ceil

public static \real ceil(\real a)

Returns the smallest (closest to negative infinity) \real value that is not less than the argument and is equal to a mathematical integer.

Parameters:

a - a value.

Returns:

the smallest (closest to negative infinity) \real value that is not less than the argument and is equal to a mathematical integer.

Specifications: pure

public normal_behavior
ensures (* \result == TBC *);

floor

public static \real floor(\real a)

Returns the largest (closest to positive infinity) \real value that is not greater than the argument and is equal to a mathematical integer.

Parameters:

a - a value.

Returns:

the largest (closest to positive infinity) \real value that is not greater than the argument and is equal to a mathematical integer.

Specifications: pure

public normal_behavior
ensures (* \result == TBC *);

rint

public static \real rint(\real a)

Returns the \real value that is closest in value to the argument and is equal to a mathematical integer. If two \real values that are mathematical integers are equally close, the result is the integer value that is even.

Parameters:

a - a \real value.

Returns:

the closest \real value to a that is equal to a mathematical integer.

Specifications: pure

public normal_behavior
ensures \result == nearestInteger(a);

nearestInteger

public static \bigint nearestInteger(\real a)

Specifications: pure

public normal_behavior
ensures abs(\result -a) <= 0.5&&abs(\result -a) == 0.5 ==> \result %2 == 0;

pow

public static \real pow(\real a,
                        \real b)

Returns of value of the first argument raised to the power of the second argument.

Parameters:

a - the base.

b - the exponent.

Returns:

the value ab.

Specifications: pure

public normal_behavior
ensures (* \result == TBC *);

round

public static \bigint round(\real a)

Returns the closest \bigint to the argument. The result is equal to the value of the expression:

JMLMath.floor(a + 0.5d)

Parameters:

a - a \real value.

Returns:

the value of the argument rounded to the nearest \bigint value, i.e.

JMLMath.floor(a + 0.5d)

.

Specifications: pure

public normal_behavior
ensures \result == (\bigint)floor(a+0.5);

abs

public static \bigint abs(\bigint a)

Returns the absolute value of a \bigint value. If the argument is not negative, the argument is returned. If the argument is negative, the negation of the argument is returned.

Parameters:

a - the argument whose absolute value is to be determined

Returns:

the absolute value of the argument.

Specifications: pure

public normal_behavior
ensures \result == ((a < 0) ? -a : a);

abs

public static \real abs(\real a)

Returns the absolute value of a \real value. If the argument is not negative, the argument is returned. If the argument is negative, the negation of the argument is returned.

Parameters:

a - the argument whose absolute value is to be determined

Returns:

the absolute value of the argument.

Specifications: pure

public normal_behavior
ensures \result == ((a < 0.0) ? -a : a);

max

public static \bigint max(\bigint a,
                          \bigint b)

Returns the greater of two \bigint values.

Parameters:

a - an argument.

b - another argument.

Returns:

the larger of a and b.

Specifications: pure

public normal_behavior
ensures \result == ((a >= b) ? a : b);

max

public static \real max(\real a,
                        \real b)

Returns the greater of two \real values.

Parameters:

a - an argument.

b - another argument.

Returns:

the larger of a and b.

Specifications: pure

public normal_behavior
ensures \result == ((a >= b) ? a : b);

min

public static \bigint min(\bigint a,
                          \bigint b)

Returns the smaller of two int values.

Parameters:

a - an argument.

b - another argument.

Returns:

the smaller of a and b.

Specifications: pure

public normal_behavior
ensures \result == ((a <= b) ? a : b);

min

public static \real min(\real a,
                        \real b)

Returns the smaller of two \real values.

Parameters:

a - an argument.

b - another argument.

Returns:

the smaller of a and b.

Specifications: pure

public normal_behavior
ensures \result == ((a <= b) ? a : b);