367 @ ensures nWords > 0 ==> data[nWords - 1] != 0;
368 @*/
369 private /*@ helper @*/ void trimLeadingZeros() {
370 int i = nWords;
371 if (i > 0 && (data[--i] == 0)) {
372 //for (; i > 0 && data[i - 1] == 0; i--) ;
373 while(i > 0 && data[i - 1] == 0) {
374 i--;
375 }
376 this.nWords = i;
377 if (i == 0) { // all words are zero
378 this.offset = 0;
379 }
380 }
381 }
382
383 /**
384 * Retrieves the normalization bias of the <code>FDBigIntger</code>. The
385 * normalization bias is a left shift such that after it the highest word
386 * of the value will have the 4 highest bits equal to zero:
387 * <code>(highestWord & 0xf0000000) == 0</code>, but the next bit should be 1
388 * <code>(highestWord & 0x08000000) != 0</code>.
389 *
390 * @return The normalization bias.
391 */
392 /*@
393 @ requires this.value() > 0;
394 @*/
395 public /*@ pure @*/ int getNormalizationBias() {
396 if (nWords == 0) {
397 throw new IllegalArgumentException("Zero value cannot be normalized");
398 }
399 int zeros = Integer.numberOfLeadingZeros(data[nWords - 1]);
400 return (zeros < 4) ? 28 + zeros : zeros - 4;
401 }
402
403 // TODO: Why is anticount param needed if it is always 32 - bitcount?
404 /**
405 * Left shifts the contents of one int array into another.
406 *
407 * @param src The source array.
408 * @param idx The initial index of the source array.
529 @
530 @ requires this.value() > 0;
531 @ ensures ((\bigint)1) << (\result - 1) <= this.value() && this.value() <= ((\bigint)1) << \result;
532 @*/
533 private /*@ pure @*/ int size() {
534 return nWords + offset;
535 }
536
537
538 /**
539 * Computes
540 * <pre>
541 * q = (int)( this / S )
542 * this = 10 * ( this mod S )
543 * Return q.
544 * </pre>
545 * This is the iteration step of digit development for output.
546 * We assume that S has been normalized, as above, and that
547 * "this" has been left-shifted accordingly.
548 * Also assumed, of course, is that the result, q, can be expressed
549 * as an integer, 0 <= q < 10.
550 *
551 * @param The divisor of this <code>FDBigInteger</code>.
552 * @return <code>q = (int)(this / S)</code>.
553 */
554 /*@
555 @ requires !this.isImmutable;
556 @ requires this.size() <= S.size();
557 @ requires this.data.length + this.offset >= S.size();
558 @ requires S.value() >= ((\bigint)1) << (S.size()*32 - 4);
559 @ assignable this.nWords, this.offset, this.data, this.data[*];
560 @ ensures \result == \old(this.value() / S.value());
561 @ ensures this.value() == \old(10 * (this.value() % S.value()));
562 @*/
563 public int quoRemIteration(FDBigInteger S) throws IllegalArgumentException {
564 assert !this.isImmutable : "cannot modify immutable value";
565 // ensure that this and S have the same number of
566 // digits. If S is properly normalized and q < 10 then
567 // this must be so.
568 int thSize = this.size();
569 int sSize = S.size();
570 if (thSize < sSize) {
571 // this value is significantly less than S, result of division is zero.
668 } else {
669 data = Arrays.copyOf(data, data.length + 1);
670 }
671 }
672 data[nWords++] = p;
673 } else {
674 trimLeadingZeros();
675 }
676 return this;
677 }
678 }
679
680 /**
681 * Multiplies this <code>FDBigInteger</code> by
682 * <code>5<sup>p5</sup> * 2<sup>p2</sup></code>. The operation will be
683 * performed in place if possible, otherwise a new <code>FDBigInteger</code>
684 * will be returned.
685 *
686 * @param p5 The exponent of the power-of-five factor.
687 * @param p2 The exponent of the power-of-two factor.
688 * @return
689 */
690 /*@
691 @ requires this.value() == 0 || p5 == 0 && p2 == 0;
692 @ assignable \nothing;
693 @ ensures \result == this;
694 @
695 @ also
696 @
697 @ requires this.value() > 0 && (p5 > 0 && p2 >= 0 || p5 == 0 && p2 > 0 && this.isImmutable);
698 @ assignable \nothing;
699 @ ensures \result.value() == \old(this.value() * pow52(p5, p2));
700 @
701 @ also
702 @
703 @ requires this.value() > 0 && p5 == 0 && p2 > 0 && !this.isImmutable;
704 @ assignable this.nWords, this.data, this.data[*];
705 @ ensures \result == this;
706 @ ensures \result.value() == \old(this.value() * pow52(p5, p2));
707 @*/
708 public FDBigInteger multByPow52(int p5, int p2) {
914 * @param a The array to be examined.
915 * @param from The index strictly below which elements are to be examined.
916 * @return Zero if all elements in range are zero, 1 otherwise.
917 */
918 /*@
919 @ requires 0 <= from && from <= a.length;
920 @ ensures \result == (AP(a, from) == 0 ? 0 : 1);
921 @*/
922 private /*@ pure @*/ static int checkZeroTail(int[] a, int from) {
923 while (from > 0) {
924 if (a[--from] != 0) {
925 return 1;
926 }
927 }
928 return 0;
929 }
930
931 /**
932 * Compares the parameter with this <code>FDBigInteger</code>. Returns an
933 * integer accordingly as:
934 * <pre>
935 * >0: this > other
936 * 0: this == other
937 * <0: this < other
938 * </pre>
939 *
940 * @param other The <code>FDBigInteger</code> to compare.
941 * @return A negative value, zero, or a positive value according to the
942 * result of the comparison.
943 */
944 /*@
945 @ ensures \result == (this.value() < other.value() ? -1 : this.value() > other.value() ? +1 : 0);
946 @*/
947 public /*@ pure @*/ int cmp(FDBigInteger other) {
948 int aSize = nWords + offset;
949 int bSize = other.nWords + other.offset;
950 if (aSize > bSize) {
951 return 1;
952 } else if (aSize < bSize) {
953 return -1;
954 }
955 int aLen = nWords;
956 int bLen = other.nWords;
957 while (aLen > 0 && bLen > 0) {
958 int a = data[--aLen];
959 int b = other.data[--bLen];
960 if (a != b) {
961 return ((a & LONG_MASK) < (b & LONG_MASK)) ? -1 : 1;
962 }
963 }
964 if (aLen > 0) {
965 return checkZeroTail(data, aLen);
966 }
967 if (bLen > 0) {
968 return -checkZeroTail(other.data, bLen);
969 }
970 return 0;
971 }
972
973 /**
974 * Compares this <code>FDBigInteger</code> with
975 * <code>5<sup>p5</sup> * 2<sup>p2</sup></code>.
976 * Returns an integer accordingly as:
977 * <pre>
978 * >0: this > other
979 * 0: this == other
980 * <0: this < other
981 * </pre>
982 * @param p5 The exponent of the power-of-five factor.
983 * @param p2 The exponent of the power-of-two factor.
984 * @return A negative value, zero, or a positive value according to the
985 * result of the comparison.
986 */
987 /*@
988 @ requires p5 >= 0 && p2 >= 0;
989 @ ensures \result == (this.value() < pow52(p5, p2) ? -1 : this.value() > pow52(p5, p2) ? +1 : 0);
990 @*/
991 public /*@ pure @*/ int cmpPow52(int p5, int p2) {
992 if (p5 == 0) {
993 int wordcount = p2 >> 5;
994 int bitcount = p2 & 0x1f;
995 int size = this.nWords + this.offset;
996 if (size > wordcount + 1) {
997 return 1;
998 } else if (size < wordcount + 1) {
999 return -1;
1000 }
1001 int a = this.data[this.nWords -1];
1002 int b = 1 << bitcount;
1003 if (a != b) {
1004 return ( (a & LONG_MASK) < (b & LONG_MASK)) ? -1 : 1;
1005 }
1006 return checkZeroTail(this.data, this.nWords - 1);
1007 }
1008 return this.cmp(big5pow(p5).leftShift(p2));
1009 }
1010
1011 /**
1012 * Compares this <code>FDBigInteger</code> with <code>x + y</code>. Returns a
1013 * value according to the comparison as:
1014 * <pre>
1015 * -1: this < x + y
1016 * 0: this == x + y
1017 * 1: this > x + y
1018 * </pre>
1019 * @param x The first addend of the sum to compare.
1020 * @param y The second addend of the sum to compare.
1021 * @return -1, 0, or 1 according to the result of the comparison.
1022 */
1023 /*@
1024 @ ensures \result == (this.value() < x.value() + y.value() ? -1 : this.value() > x.value() + y.value() ? +1 : 0);
1025 @*/
1026 public /*@ pure @*/ int addAndCmp(FDBigInteger x, FDBigInteger y) {
1027 FDBigInteger big;
1028 FDBigInteger small;
1029 int xSize = x.size();
1030 int ySize = y.size();
1031 int bSize;
1032 int sSize;
1033 if (xSize >= ySize) {
1034 big = x;
1035 small = y;
1036 bSize = xSize;
1037 sSize = ySize;
1038 } else {
|
367 @ ensures nWords > 0 ==> data[nWords - 1] != 0;
368 @*/
369 private /*@ helper @*/ void trimLeadingZeros() {
370 int i = nWords;
371 if (i > 0 && (data[--i] == 0)) {
372 //for (; i > 0 && data[i - 1] == 0; i--) ;
373 while(i > 0 && data[i - 1] == 0) {
374 i--;
375 }
376 this.nWords = i;
377 if (i == 0) { // all words are zero
378 this.offset = 0;
379 }
380 }
381 }
382
383 /**
384 * Retrieves the normalization bias of the <code>FDBigIntger</code>. The
385 * normalization bias is a left shift such that after it the highest word
386 * of the value will have the 4 highest bits equal to zero:
387 * {@code (highestWord & 0xf0000000) == 0}, but the next bit should be 1
388 * {@code (highestWord & 0x08000000) != 0}.
389 *
390 * @return The normalization bias.
391 */
392 /*@
393 @ requires this.value() > 0;
394 @*/
395 public /*@ pure @*/ int getNormalizationBias() {
396 if (nWords == 0) {
397 throw new IllegalArgumentException("Zero value cannot be normalized");
398 }
399 int zeros = Integer.numberOfLeadingZeros(data[nWords - 1]);
400 return (zeros < 4) ? 28 + zeros : zeros - 4;
401 }
402
403 // TODO: Why is anticount param needed if it is always 32 - bitcount?
404 /**
405 * Left shifts the contents of one int array into another.
406 *
407 * @param src The source array.
408 * @param idx The initial index of the source array.
529 @
530 @ requires this.value() > 0;
531 @ ensures ((\bigint)1) << (\result - 1) <= this.value() && this.value() <= ((\bigint)1) << \result;
532 @*/
533 private /*@ pure @*/ int size() {
534 return nWords + offset;
535 }
536
537
538 /**
539 * Computes
540 * <pre>
541 * q = (int)( this / S )
542 * this = 10 * ( this mod S )
543 * Return q.
544 * </pre>
545 * This is the iteration step of digit development for output.
546 * We assume that S has been normalized, as above, and that
547 * "this" has been left-shifted accordingly.
548 * Also assumed, of course, is that the result, q, can be expressed
549 * as an integer, {@code 0 <= q < 10}.
550 *
551 * @param S The divisor of this <code>FDBigInteger</code>.
552 * @return <code>q = (int)(this / S)</code>.
553 */
554 /*@
555 @ requires !this.isImmutable;
556 @ requires this.size() <= S.size();
557 @ requires this.data.length + this.offset >= S.size();
558 @ requires S.value() >= ((\bigint)1) << (S.size()*32 - 4);
559 @ assignable this.nWords, this.offset, this.data, this.data[*];
560 @ ensures \result == \old(this.value() / S.value());
561 @ ensures this.value() == \old(10 * (this.value() % S.value()));
562 @*/
563 public int quoRemIteration(FDBigInteger S) throws IllegalArgumentException {
564 assert !this.isImmutable : "cannot modify immutable value";
565 // ensure that this and S have the same number of
566 // digits. If S is properly normalized and q < 10 then
567 // this must be so.
568 int thSize = this.size();
569 int sSize = S.size();
570 if (thSize < sSize) {
571 // this value is significantly less than S, result of division is zero.
668 } else {
669 data = Arrays.copyOf(data, data.length + 1);
670 }
671 }
672 data[nWords++] = p;
673 } else {
674 trimLeadingZeros();
675 }
676 return this;
677 }
678 }
679
680 /**
681 * Multiplies this <code>FDBigInteger</code> by
682 * <code>5<sup>p5</sup> * 2<sup>p2</sup></code>. The operation will be
683 * performed in place if possible, otherwise a new <code>FDBigInteger</code>
684 * will be returned.
685 *
686 * @param p5 The exponent of the power-of-five factor.
687 * @param p2 The exponent of the power-of-two factor.
688 * @return The multiplication result.
689 */
690 /*@
691 @ requires this.value() == 0 || p5 == 0 && p2 == 0;
692 @ assignable \nothing;
693 @ ensures \result == this;
694 @
695 @ also
696 @
697 @ requires this.value() > 0 && (p5 > 0 && p2 >= 0 || p5 == 0 && p2 > 0 && this.isImmutable);
698 @ assignable \nothing;
699 @ ensures \result.value() == \old(this.value() * pow52(p5, p2));
700 @
701 @ also
702 @
703 @ requires this.value() > 0 && p5 == 0 && p2 > 0 && !this.isImmutable;
704 @ assignable this.nWords, this.data, this.data[*];
705 @ ensures \result == this;
706 @ ensures \result.value() == \old(this.value() * pow52(p5, p2));
707 @*/
708 public FDBigInteger multByPow52(int p5, int p2) {
914 * @param a The array to be examined.
915 * @param from The index strictly below which elements are to be examined.
916 * @return Zero if all elements in range are zero, 1 otherwise.
917 */
918 /*@
919 @ requires 0 <= from && from <= a.length;
920 @ ensures \result == (AP(a, from) == 0 ? 0 : 1);
921 @*/
922 private /*@ pure @*/ static int checkZeroTail(int[] a, int from) {
923 while (from > 0) {
924 if (a[--from] != 0) {
925 return 1;
926 }
927 }
928 return 0;
929 }
930
931 /**
932 * Compares the parameter with this <code>FDBigInteger</code>. Returns an
933 * integer accordingly as:
934 * <pre>{@code
935 * > 0: this > other
936 * 0: this == other
937 * < 0: this < other
938 * }</pre>
939 *
940 * @param other The <code>FDBigInteger</code> to compare.
941 * @return A negative value, zero, or a positive value according to the
942 * result of the comparison.
943 */
944 /*@
945 @ ensures \result == (this.value() < other.value() ? -1 : this.value() > other.value() ? +1 : 0);
946 @*/
947 public /*@ pure @*/ int cmp(FDBigInteger other) {
948 int aSize = nWords + offset;
949 int bSize = other.nWords + other.offset;
950 if (aSize > bSize) {
951 return 1;
952 } else if (aSize < bSize) {
953 return -1;
954 }
955 int aLen = nWords;
956 int bLen = other.nWords;
957 while (aLen > 0 && bLen > 0) {
958 int a = data[--aLen];
959 int b = other.data[--bLen];
960 if (a != b) {
961 return ((a & LONG_MASK) < (b & LONG_MASK)) ? -1 : 1;
962 }
963 }
964 if (aLen > 0) {
965 return checkZeroTail(data, aLen);
966 }
967 if (bLen > 0) {
968 return -checkZeroTail(other.data, bLen);
969 }
970 return 0;
971 }
972
973 /**
974 * Compares this <code>FDBigInteger</code> with
975 * <code>5<sup>p5</sup> * 2<sup>p2</sup></code>.
976 * Returns an integer accordingly as:
977 * <pre>{@code
978 * > 0: this > other
979 * 0: this == other
980 * < 0: this < other
981 * }</pre>
982 * @param p5 The exponent of the power-of-five factor.
983 * @param p2 The exponent of the power-of-two factor.
984 * @return A negative value, zero, or a positive value according to the
985 * result of the comparison.
986 */
987 /*@
988 @ requires p5 >= 0 && p2 >= 0;
989 @ ensures \result == (this.value() < pow52(p5, p2) ? -1 : this.value() > pow52(p5, p2) ? +1 : 0);
990 @*/
991 public /*@ pure @*/ int cmpPow52(int p5, int p2) {
992 if (p5 == 0) {
993 int wordcount = p2 >> 5;
994 int bitcount = p2 & 0x1f;
995 int size = this.nWords + this.offset;
996 if (size > wordcount + 1) {
997 return 1;
998 } else if (size < wordcount + 1) {
999 return -1;
1000 }
1001 int a = this.data[this.nWords -1];
1002 int b = 1 << bitcount;
1003 if (a != b) {
1004 return ( (a & LONG_MASK) < (b & LONG_MASK)) ? -1 : 1;
1005 }
1006 return checkZeroTail(this.data, this.nWords - 1);
1007 }
1008 return this.cmp(big5pow(p5).leftShift(p2));
1009 }
1010
1011 /**
1012 * Compares this <code>FDBigInteger</code> with <code>x + y</code>. Returns a
1013 * value according to the comparison as:
1014 * <pre>{@code
1015 * -1: this < x + y
1016 * 0: this == x + y
1017 * 1: this > x + y
1018 * }</pre>
1019 * @param x The first addend of the sum to compare.
1020 * @param y The second addend of the sum to compare.
1021 * @return -1, 0, or 1 according to the result of the comparison.
1022 */
1023 /*@
1024 @ ensures \result == (this.value() < x.value() + y.value() ? -1 : this.value() > x.value() + y.value() ? +1 : 0);
1025 @*/
1026 public /*@ pure @*/ int addAndCmp(FDBigInteger x, FDBigInteger y) {
1027 FDBigInteger big;
1028 FDBigInteger small;
1029 int xSize = x.size();
1030 int ySize = y.size();
1031 int bSize;
1032 int sSize;
1033 if (xSize >= ySize) {
1034 big = x;
1035 small = y;
1036 bSize = xSize;
1037 sSize = ySize;
1038 } else {
|