算法。将两个n位二进制数相加。这个问题的循环不变性是什么？

Question

我正在解决CLRS《算法导论》中的练习2.1-4。

这个问题描述为

考虑将两个n位二进制整数相加的问题 储存在两个n元素数组A和B中 两个整数的和应该以二进制形式储存在元素数组C中

这个问题的循环不变性是什么？对于这个问题，我有一些想法，作为注释写在我用golang写的这个问题的解决方案中。

package additoin_binary

/*
Loop invariant:
At the start of each iteration of the loop digits in the subarray r[len(r) - 1 - i:] are
a[len(a) - 1 - i:] + b[len(b) - 1 - i:] + carry | provided that (len(a) - 1 - i) and (len(b) - 1 - i) are positive
a[len(a) - 1 - i:] + carry                      | provided that (len(a) - 1 - i) is positive and (len(b) - 1 - i) is negative
carry                                           | provided that (len(a) - 1 - i) and (len(b) - 1 - i) are negative
*** carry for i = a[(len(a) - 1) - i - 1] + b[(len(b) - 1) - i - 1] == 2 ? 1 : 0
*/

func BinaryAddition(a, b []int) []int {
    // a and b can have arbitrary number of digits.
    // We should control a length of the second term. It should be less or equal to a length of first term.w
    // Other vise we swap them
    if len(b) > len(a) {
        b, a = a, b
    }
    // loop invariant initialization:
    // before first loop iteration (i=0) index b_i is out of the array range (b[-1]),  so we don't have second term and sum = a
    // another way of thinking about it is we don't get b as argument and then sum = a, too
    if len(b) == 0 {
        return a
    }
    // result array to store sum
    r := make([]int, len(a)+1)
    // overflow of summing two bits (1 + 1)
    carry := 0
    // loop invariant maintenance:
    // we have right digits (after addition) in r for indexes r[len(r) - 1 - i:]
    for i := 0; i < len(r); i++ {
        a_i := len(a) - 1 - i // index for getting a last digit of a
        b_i := len(b) - 1 - i // index for getting a last digit of b
        r_i := len(r) - 1 - i // index for getting a last digit of r

        var s int
        if b_i >= 0 && a_i >= 0 {
            s = a[a_i] + b[b_i] + carry
        } else if a_i >= 0 {
            s = a[a_i] + carry
        } else { // all indexes run out of the game (a < 0, b < 0)
            s = carry
        }

        if s > 1 {
            r[r_i] = 0
            carry = 1
        } else {
            r[r_i] = s
            carry = 0
        }
    }
    // loop invariant termination:
    // i goes from 0 to len(r) - 1, r[len(r) - 1 - ([len(r) - 1):] => r[:]
    // This means, that for every index in r we have a right sum
    //*At i=0, r[i] a sum can be equal to 0, so we explicitly check that before return r
    if r[0] == 0 {
        return r[1:]
    } else {
        return r
    }
}

编辑1: 我对原来的问题进行了扩展 所以现在数组A和B可以有任意长度，分别是m和n。 例子A=[1,0,1]，B=[1,0](m=3，n=2)

Answer 1

考虑将两个n位二进制整数相加的问题，存储在两个n元素数组A和B中，两个整数之和应以二进制形式存储在元素数组C中。

这个问题有一个保证，A和B是n元素数组，我认为这是一个重要的条件，可以减少代码工作量。

什么是循环不变式？

简单来说，循环不变性就是一些前提条件（条件），在循环的每一次迭代中都成立。

在这个问题中，如果假设 len = len(C)迭代 i 在 [0, len)循环不变性是 r[len-1-i:len] 始终是 a[len-2-i:len-1] 和 b[len-2-i:len-1] 在较低 i + 1 位。因为每一次循环之后，你会使一个位正确，就可以证明算法是正确的。