001: // @(#)$Id: JMLMath.java 1.2 Fri, 06 May 2005 15:27:39 +0200 engelc $
002:
003: // Copyright (C) 2003 Iowa State University
004: // Copyright (C) 2002 Sun Microsystems, Inc.
005:
006: // This file is part of JML.
007:
008: // JML is free software; you can redistribute it and/or modify
009: // it under the terms of the GNU General Public License as published by
010: // the Free Software Foundation; either version 2, or (at your option)
011: // any later version.
012:
013: // JML is distributed in the hope that it will be useful,
014: // but WITHOUT ANY WARRANTY; without even the implied warranty of
015: // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
016: // GNU General Public License for more details.
017:
018: // You should have received a copy of the GNU General Public License
019: // along with JML; see the file COPYING. If not, write to
020: // the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
021:
022: package org.jmlspecs.models;
023:
024: import java.lang.Math; // FIXME - Necessary to avoid a warning that the link to java.lang.Math cannot be found.
025:
026: /** A JML class that implements methods equivalent to those available in
027: * {@link java.lang.Math} but that are defined over <code>\bigint</code> and
028: * <code>\real</code> instead.
029: *
030: * @version $Revision: 1.2 $
031: * @author Patrice Chalin
032: * @see java.lang.Math
033: * <!--see JMLBigint-->
034: * <!--see JMLReal-->
035: */
036: //-@ immutable
037: public/*@ pure @*/final strictfp class JMLMath {
038:
039: /**
040: * The <code>\real</code> value that is closer than any other to
041: * <i>e</i>, the base of the natural logarithms. !FIXME! define exactly.
042: */
043: // -- @ public static final \real E;
044: // error: Final field "E" may not have been initialized [JLS2 8.3.1.2]
045: /**
046: * The <code>\real</code> value that is closer than any other to
047: * <i>pi</i>, the ratio of the circumference of a circle to its
048: * diameter. !FIXME! define exactly.
049: */
050: // -- @ public static final \real PI;
051: // Trig functions, etc.
052: /**
053: * Returns the correctly rounded positive square root of a
054: * <code>\real</code> value.
055: *
056: * @param a a value.
057: * <!--@return the value of √ <code>a</code>.-->
058: * @return the positive square root of <code>a</code>.
059: */
060: /*@
061: @ public normal_behavior
062: @ ensures \result > 0 && \result * \result == a;
063: @
064: @ model public static pure \real sqrt(\real a);
065: @*/
066:
067: /**
068: * Returns the smallest (closest to negative infinity)
069: * <code>\real</code> value that is not less than the argument and is
070: * equal to a mathematical integer.
071: *
072: * @param a a value.
073: * <!--@return the value ⌈ <code>a</code> ⌉.-->
074: * @return the smallest (closest to negative infinity)
075: * <code>\real</code> value that is not less than the argument
076: * and is equal to a mathematical integer.
077: */
078: /*@
079: @ public normal_behavior
080: @ ensures (* \result == TBC *);
081: @
082: @ model public static pure \real ceil(\real a);
083: @*/
084:
085: /**
086: * Returns the largest (closest to positive infinity)
087: * <code>\real</code> value that is not greater than the argument and
088: * is equal to a mathematical integer.
089: *
090: * @param a a value.
091: * <!--@return the value ⌊ <code>a</code> ⌋.-->
092: * @return the largest (closest to positive infinity)
093: * <code>\real</code> value that is not greater than the argument
094: * and is equal to a mathematical integer.
095: */
096: /*@
097: @ public normal_behavior
098: @ requires true;
099: @
100: @ model public static pure \real floor(\real a);
101: @*/
102:
103: /**
104: * Returns the <code>\real</code> value that is closest in value
105: * to the argument and is equal to a mathematical integer. If two
106: * <code>\real</code> values that are mathematical integers are
107: * equally close, the result is the integer value that is
108: * even.
109: *
110: * @param a a <code>\real</code> value.
111: * @return the closest <code>\real</code> value to <code>a</code> that is
112: * equal to a mathematical integer.
113: */
114: /*@
115: @ public normal_behavior
116: @ ensures \result == nearestInteger(a);
117: @
118: @ model public static pure \real rint(\real a);
119: @*/
120:
121: /*@
122: @ public normal_behavior
123: @ ensures abs(\result - a) <= 0.5 &&
124: @ abs(\result - a) == 0.5 ==> \result % 2 == 0;
125: @
126: @ model public static pure \bigint nearestInteger(\real a);
127: @*/
128:
129: // atan2 - TBC.
130: /**
131: * Returns of value of the first argument raised to the power of the
132: * second argument.
133: *
134: * @param a the base.
135: * @param b the exponent.
136: * @return the value <code>a<sup>b</sup></code>.
137: */
138: /*@
139: @ public normal_behavior
140: @ ensures (* \result == TBC *);
141: @*/
142: //@ model public static pure \real pow(\real a, \real b);
143: /**
144: * Returns the closest <code>\bigint</code> to the argument. The result is
145: * equal to the value of the expression:
146: * <p><pre>JMLMath.floor(a + 0.5d)</pre>
147: *
148: * @param a a <code>\real</code> value.
149: * @return the value of the argument rounded to the nearest
150: * <code>\bigint</code> value, i.e. <pre>JMLMath.floor(a + 0.5d)</pre>.
151: */
152: /*@
153: @ public normal_behavior
154: @ ensures \result == (\bigint)floor(a + 0.5d);
155: @
156: @ model public static pure \bigint round(\real a) {
157: @ return (\bigint)floor(a + 0.5d);
158: @ }
159: @*/
160:
161: // Random number gen ... TBC.
162: /**
163: * Returns the absolute value of a <code>\bigint</code> value.
164: * If the argument is not negative, the argument is returned.
165: * If the argument is negative, the negation of the argument is returned.
166: *
167: * @param a the argument whose absolute value is to be determined
168: * @return the absolute value of the argument.
169: */
170: /*@
171: @ public normal_behavior
172: @ ensures \result == ((a < 0) ? -a : a);
173: @
174: @ model public static pure \bigint abs(\bigint a) {
175: @ return (a < 0) ? -a : a;
176: @ }
177: @*/
178:
179: /**
180: * Returns the absolute value of a <code>\real</code> value.
181: * If the argument is not negative, the argument is returned.
182: * If the argument is negative, the negation of the argument is returned.
183: *
184: * @param a the argument whose absolute value is to be determined
185: * @return the absolute value of the argument.
186: */
187: /*@
188: @ public normal_behavior
189: @ ensures \result == ((a < 0) ? - a : a);
190: @
191: @ model public static pure \real abs(\real a) {
192: @ return (a < 0) ? - a : a;
193: @ }
194: @*/
195:
196: /**
197: * Returns the greater of two <code>\bigint</code> values.
198: *
199: * @param a an argument.
200: * @param b another argument.
201: * @return the larger of <code>a</code> and <code>b</code>.
202: */
203: /*@
204: @ public normal_behavior
205: @ ensures \result == ((a >= b) ? a : b);
206: @
207: @ model public static pure \bigint max(\bigint a, \bigint b) {
208: @ return (a >= b) ? a : b;
209: @ }
210: @*/
211:
212: /**
213: * Returns the greater of two <code>\real</code> values.
214: *
215: * @param a an argument.
216: * @param b another argument.
217: * @return the larger of <code>a</code> and <code>b</code>.
218: */
219: /*@
220: @ public normal_behavior
221: @ ensures \result == ((a >= b) ? a : b);
222: @
223: @ model public static pure \real max(\real a, \real b) {
224: @ return (a >= b) ? a : b;
225: @ }
226: @*/
227:
228: /**
229: * Returns the smaller of two <code>int</code> values.
230: *
231: * @param a an argument.
232: * @param b another argument.
233: * @return the smaller of <code>a</code> and <code>b</code>.
234: */
235: /*@
236: @ public normal_behavior
237: @ ensures \result == ((a <= b) ? a : b);
238: @
239: @ model public static pure \bigint min(\bigint a, \bigint b) {
240: @ return (a <= b) ? a : b;
241: @ }
242: @*/
243:
244: /**
245: * Returns the smaller of two <code>\real</code> values.
246: *
247: * @param a an argument.
248: * @param b another argument.
249: * @return the smaller of <code>a</code> and <code>b</code>.
250: */
251: /*@
252: @ public normal_behavior
253: @ ensures \result == ((a <= b) ? a : b);
254: @
255: @ model public static pure \real min(\real a, \real b) {
256: @ return (a <= b) ? a : b;
257: @ }
258: @*/
259:
260: /**
261: * Don't let anyone instantiate this class.
262: */
263: private JMLMath() {
264: }
265:
266: }
|