■

正の整数A,B,Cの正の和のオーバーフローについて詳しく考える。
まず32bit値の変数を考えたときオーバーフローを起こすのは数値が2^32以上の値になった時であるのでその境界値をMと置く。
するとA+B+Cのオーバーフローは以下のように考えられる

B+Cがオーバーフローをする
もしくは
B+Cがオーバーフローせず　かつ　A+(B+C)がオーバーフローをする
時
A+B+Cはオーバーフローをする。
簡単のため、オーバーフローをするという述語を「⇒OF」、
オーバーフローしないという述語を「!⇒OF」と置き換えると

「B+C ⇒ OF || ( B+C !⇒ OF && A+(B+C) ⇒ OF)」⇒「A+B+C ⇒ OF」
である事がいえる。
すなわち
「B+C ⇒ OF || ( B+C !⇒ OF && A+(B+C) ⇒ OF)」は「A+B+C⇒OF」の
十分条件になっている。
これからこの逆（必要条件）を証明する。

「A+B+C⇒OF」であるとすると以下のどれかが成り立つ
「A+B ⇒ OF || ( A+B !⇒ OF && (A+B)+C ⇒ OF)」... ①
「B+C ⇒ OF || ( B+C !⇒ OF && A+(B+C) ⇒ OF)」... ②
「C+A ⇒ OF || ( C+A !⇒ OF && (C+A)+B ⇒ OF)」... ③
もし①と②と③が同意であれば求める命題が証明される。

また、対象性より①⇔②ならば同様に②⇔③、①⇔③が成り立つ。
よって①⇔②を証明する。

①であると仮定し、B+CのOF状態で場合分けする
1) B+C ⇒ OF
　これは②の条件を満たしているので真
2) B+C !⇒ OF
 ①の前半の条件の場合 (A+B ⇒ OF)
  B+C < M, A+B >= Mが言えてこれより
  A+(B+C) = (A+B)+C >= M
 すなわち A+(B+C) ⇒ OF
 ①の後半の条件の場合 (A+B !⇒ OF && (A+B)+C ⇒ OF)
  B+C < M, A+B < M, (A+B)+C >= M
 これより
  A+(B+C) = (A+B)+C >= M
 すなわち A+(B+C) ⇒ OF
よって①⇒②は満たされた。

②であると仮定するとこれはA+B+C ⇒ OFである事は明らか

以上より求める命題は証明された。

これから多倍長整数の剰余算以外を実装
以下その一部

template <typename L>
bool BIGINT<L>::isCarryOutPlus(L x, L y, L carry)
{
  L temp = y + carry;
  if (temp < y)
    return true;
  else if (x + temp < x)
    return true;

  return false;
}

template <typename L>
BIGINT<L> BIGINT<L>::operator+(const BIGINT<L>& org)
{
  BIGINT<L> retInt;
  list<L>   temp;

  list<L>   lint2 = org.getLint();
  int       degree2 = org.getDegree();
  bool      sign2   = org.getSign();

  int       longDegree;
  bool      longSign, smallSign;
  typename list<L>::iterator iLong, iLongEnd, iSmall, iSmallEnd;
  if (*this >= org) {
    iLong = lint.begin();
    iSmall = lint2.begin();
    iLongEnd = lint.end();
    iSmallEnd = lint2.end();
    longDegree = degree;
    longSign = sign;
    smallSign = sign2;
  } else {
    iLong = lint2.begin();
    iSmall = lint.begin();
    iLongEnd = lint2.end();
    iSmallEnd = lint.end();
    longDegree = degree2;
    longSign = sign2;
    smallSign = sign;
  }
  L carry = 0;

  if (sign == sign2) {
    L small;
    while (iLong != iLongEnd) {
      if (iSmall == iSmallEnd)
        small = 0;
      else
        small = *iSmall;

      temp.push_back(*iLong + small + carry);

      if (isCarryOutPlus(*iLong, small, carry))
        carry = 1;
      else
        carry = 0;

      iLong++;
      if (iSmall != iSmallEnd)
        iSmall++;
    }

    if (carry != 0) {
      temp.push_back(carry);
      retInt.setDegree(longDegree+1);
    } else
      retInt.setDegree(longDegree);

    retInt.setSign(sign);
  } else { // sign != sign2

    L small;
    while (iLong != iLongEnd) {
      if (iSmall == iSmallEnd)
        small = 0;
      else
        small = *iSmall;

      /* example
       * 1000 - 100 = 900 ... carry = 0
       * 100 - 1000 = 4294966396 ... carry = 1
       * 0 - 4294967295 - 1 = 0 ... carry = 1
       * 0 - 4294967295 = 1 ... carry = 1
       */
      temp.push_back(*iLong - small - carry);

      if (isCarryOutMinus(*iLong, small, carry))
        carry = 1;
      else
        carry = 0;

      iLong++;
      if (iSmall != iSmallEnd)
        iSmall++;
    }

    // Because of checking size between lint and lint2,
    // the BIGINT of return must have the longSign.
    retInt.setSign(longSign);

    if (temp.front() == 0) {
      temp.erase(temp.begin());
      retInt.setDegree(longDegree-1);
    } else {
      retInt.setDegree(longDegree);
    }
  }

  retInt.setLint(temp);
  return retInt;
}