001: // @(#)$Id: BigInteger.java 1.1 Mon, 09 May 2005 15:39:51 +0200 engelc $
002:
003: // Copyright (C) 2001 Iowa State University
004:
005: // This file is part of JML
006:
007: // JML is free software; you can redistribute it and/or modify
008: // it under the terms of the GNU General Public License as published by
009: // the Free Software Foundation; either version 2, or (at your option)
010: // any later version.
011:
012: // JML is distributed in the hope that it will be useful,
013: // but WITHOUT ANY WARRANTY; without even the implied warranty of
014: // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
015: // GNU General Public License for more details.
016:
017: // You should have received a copy of the GNU General Public License
018: // along with JML; see the file COPYING. If not, write to
019: // the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
020:
021: package java.math;
022:
023: import java.util.Random;
024:
025: /** JML's specification of java.math.BigInteger.
026: *
027: * @version $Revision: 1.1 $
028: * @author David R. Cok
029: * @author Gary T. Leavens
030: */
031: //-@ immutable
032: public/*@ pure @*/class BigInteger extends Number implements
033: Comparable {
034:
035: /*@
036: public normal_behavior
037: ensures \result.equals(new BigInteger(val, radix));
038: public static model pure BigInteger parse(String val, int radix);
039: @*/
040: /*@
041: public normal_behavior
042: ensures \result.equals(new BigInteger(val));
043: public static model pure BigInteger convert(byte[] val);
044: @*/
045:
046: //--- public model \bigint value; --
047: //@ public model int sign;
048: //@ public represents sign <- signum();
049: //@ public invariant sign == compareTo(ZERO);
050:
051: /*@ public normal_behavior
052: @ requires val != null;
053: @ requires val.length != 0;
054: @ also public exceptional_behavior
055: @ requires val != null;
056: @ requires val.length == 0;
057: @ signals (java.lang.NumberFormatException);
058: @ also public exceptional_behavior
059: @ requires val == null;
060: @ signals (java.lang.NullPointerException);
061: @*/
062: public BigInteger(/*@ non_null @*/byte[] val) {
063: }
064:
065: /*@ public normal_behavior
066: @ requires magnitude != null;
067: @ requires signum == 0 || signum == 1 || signum == -1;
068: @ requires signum == 0 <==> convert(magnitude).equals(ZERO);
069: @ ensures sign == signum;
070: @*/
071: public BigInteger(int signum, /*@ non_null @*/byte[] magnitude) {
072: }
073:
074: /*@ public normal_behavior
075: @ requires val != null && !val.equals("");
076: @ requires radix > 1;
077: @ ensures this.equals(parse(val,radix));
078: @ also
079: @ public exceptional_behavior
080: @ requires val != null && val.equals("");
081: @ signals (java.lang.NumberFormatException);
082: @ also
083: @ public exceptional_behavior
084: @ requires val == null;
085: @ signals (java.lang.NullPointerException);
086: @*/
087: public BigInteger(String val, int radix) {
088: }
089:
090: /*@ normal_behavior
091: @ ensures true;
092: @*/
093: BigInteger(char[] val) {
094: }
095:
096: /*@ public normal_behavior
097: @ requires val != null && !val.equals("");
098: @ ensures this.equals(parse(val,10));
099: @ also
100: @ public exceptional_behavior
101: @ requires val.equals("");
102: @ signals (java.lang.NumberFormatException);
103: @ also
104: @ public exceptional_behavior
105: @ requires val == null;
106: @ signals (java.lang.NullPointerException);
107: @*/
108: public BigInteger(String val) {
109: }
110:
111: public BigInteger(int numBits, Random rnd) {
112: }
113:
114: public BigInteger(int bitLength, int certainty, Random rnd) {
115: }
116:
117: public BigInteger(long val) {
118: }
119:
120: public static/*@ pure @*/BigInteger probablePrime(int bitLength,
121: Random rnd) {
122: }
123:
124: boolean primeToCertainty(int certainty) {
125: }
126:
127: int jacobiSymbol(int p, BigInteger n) {
128: }
129:
130: // not sure where MutableBigInteger comes from
131: // BigInteger(MutableBigInteger val, int sign);
132:
133: //Static Factory Methods
134:
135: public static/*@ pure @*/BigInteger valueOf(long val) {
136: }
137:
138: int signum;
139: int[] mag;
140: public static final BigInteger ZERO;
141: public static final BigInteger ONE;
142:
143: //@ public invariant ZERO != null && ZERO.equals(valueOf(0));
144: //@ public invariant ZERO.equals(ZERO);
145: //@ public constraint ZERO == \old(ZERO);
146: //@ public invariant ONE != null && ONE.equals(valueOf(1));
147: //@ public invariant ONE.equals(ONE);
148: //@ public invariant !ZERO.equals(ONE);
149: //@ public constraint ONE == \old(ONE);
150:
151: // Arithmetic Operations
152:
153: //@ requires val != null;
154: public BigInteger add(BigInteger val) {
155: }
156:
157: /*@ requires val != null;
158: @ ensures equals(\result.add(val));
159: @*/
160: public BigInteger subtract(BigInteger val) {
161: }
162:
163: //@ requires val != null;
164: public BigInteger multiply(BigInteger val) {
165: }
166:
167: /*@ requires val != null;
168: @ ensures equals(\result.multiply(val).add(remainder(val)));
169: @*/
170: public BigInteger divide(BigInteger val) {
171: }
172:
173: /*@ ensures \result[0].equals(divide(val));
174: @ ensures \result[1].equals(remainder(val));
175: @*/
176: public BigInteger[] divideAndRemainder(BigInteger val) {
177: }
178:
179: public BigInteger remainder(BigInteger val) {
180: }
181:
182: public BigInteger pow(int exponent) {
183: }
184:
185: public BigInteger gcd(BigInteger val) {
186: }
187:
188: static void primitiveRightShift(int[] a, int len, int n) {
189: }
190:
191: static void primitiveLeftShift(int[] a, int len, int n) {
192: }
193:
194: /*@ assignable \nothing;
195: @ ensures \result.signum() >= 0 && (sign==0 ==> \result.signum() == 0);
196: @*/
197: public BigInteger abs() {
198: }
199:
200: /*@ assignable \nothing;
201: @ ensures \result.signum() == - sign;
202: @*/
203: public BigInteger negate() {
204: }
205:
206: //@ ensures \result == sign;
207: public int signum() {
208: }
209:
210: // Modular Arithmetic Operations
211:
212: public BigInteger mod(BigInteger m) {
213: }
214:
215: public BigInteger modPow(BigInteger exponent, BigInteger m) {
216: }
217:
218: static int[] bnExpModThreshTable;
219:
220: static int mulAdd(int[] out, int[] in, int offset, int len, int k) {
221: }
222:
223: static int addOne(int[] a, int offset, int mlen, int carry) {
224: }
225:
226: public BigInteger modInverse(BigInteger m) {
227: }
228:
229: // Shift Operations
230:
231: public BigInteger shiftLeft(int n) {
232: }
233:
234: public BigInteger shiftRight(int n) {
235: }
236:
237: int[] javaIncrement(int[] val) {
238: }
239:
240: // Bitwise Operations
241:
242: public BigInteger and(BigInteger val) {
243: }
244:
245: public BigInteger or(BigInteger val) {
246: }
247:
248: public BigInteger xor(BigInteger val) {
249: }
250:
251: public BigInteger not() {
252: }
253:
254: public BigInteger andNot(BigInteger val) {
255: }
256:
257: // Single Bit Operations
258:
259: public boolean testBit(int n) {
260: }
261:
262: public BigInteger setBit(int n) {
263: }
264:
265: public BigInteger clearBit(int n) {
266: }
267:
268: public BigInteger flipBit(int n) {
269: }
270:
271: public int getLowestSetBit() {
272: }
273:
274: // Miscellaneous Bit Operations
275:
276: public int bitLength() {
277: }
278:
279: static int bitLen(int w) {
280: }
281:
282: static final byte[] trailingZeroTable;
283:
284: public int bitCount() {
285: }
286:
287: static int bitCnt(int val) {
288: }
289:
290: static int trailingZeroCnt(int val) {
291: }
292:
293: // Primality Testing
294:
295: public boolean isProbablePrime(int certainty) {
296: }
297:
298: // Comparison Operations
299:
300: public int compareTo(BigInteger val) {
301: }
302:
303: public int compareTo(Object o) {
304: }
305:
306: /*@ also public normal_behavior
307: @ requires x != null && x instanceof BigInteger;
308: @ assignable \nothing;
309: @ ensures \result == x.equals(this);
310: @*/
311: public/*@ pure @*/boolean equals(Object x) {
312: }
313:
314: public BigInteger min(BigInteger val) {
315: }
316:
317: public BigInteger max(BigInteger val) {
318: }
319:
320: // Hash Function
321:
322: public int hashCode() {
323: }
324:
325: /*@ ensures \result != null;
326: @ ensures parse(\result,radix).equals(this);
327: @*/
328: public String toString(int radix) {
329: }
330:
331: /*@ also
332: @ ensures \result != null;
333: @ ensures parse(\result,10).equals(this);
334: @*/
335: public String toString() {
336: }
337:
338: /*@ ensures convert(\result).equals(this);
339: @ ensures_redundantly this.equals(\old(this));
340: @*/
341: public byte[] toByteArray() {
342: }
343:
344: /*@ also
345: @ ensures_redundantly this.equals(\old(this));
346: @*/
347: public int intValue() {
348: }
349:
350: /*@ also
351: @ ensures_redundantly this.equals(\old(this));
352: @*/
353: public long longValue() {
354: }
355:
356: /*@ also
357: @ ensures_redundantly this.equals(\old(this));
358: @*/
359: public float floatValue() {
360: }
361:
362: /*@ also
363: @ ensures_redundantly this.equals(\old(this));
364: @*/
365: public double doubleValue() {
366: }
367:
368: }
|