# Loop invariant for adding 2 arrays storing binary value of integer

### Question:

Given 2 arrays of size $n$, $A = \langle a_1,a_2,\dots,a_n \rangle$ and $B = \langle b_1,b_2,\dots,b_n\rangle$, where $A$ and $B$ store the binary value of an integer. Find $A + B$ and stores the result in array $C$ of size $[n+1]$, $C = \langle c_1,c_2,\dots,c_{n+1}\rangle$.

### Pseudocode:

ADD-BINARY(A,B)
C = new integer[A.length + 1]
carry = 0

for i = A.length to i = 1
C[i] = (A[i] + B[i] + carry) % 2
carry = (A[i] + B[i] + carry) / 2

C[1] = carry

return c


After writing the pseudo-code, I'm trying to find the loop invariant. One of the statement I can think of is

At the start of each iteration in the for loop, C[A.length...i] consists of the sum of binary A[A.length...i] and B[A.length...i].

But I check the initialization stage and found out that it is invalid because at the beginning of the for loop C[A.length] does not have the sum yet(it just got initialized). So I'm puzzled whether I'm approaching it the right way.

• C[A.length...i] seems to be entirely wrong. For example, if A.length = 10, i = 5, are you trying to say something about C [10..5] ? And "carry" should be in there somewhere. Jun 25, 2017 at 6:33
• Yes. And I don't understand your second statement, mind elaborating? Jun 25, 2017 at 6:45
• It is only at the iteration i that you set c[i], so at the start of the iteration, c[i] cannot be taken into account in your invariant. This is the right idea, but there might be an off-by-one (plus as already pointed out, the variable carry should also appear in your invariant).
– md5
Jun 25, 2017 at 9:56
• @md5 you are right, that's why I think my invariant is wrong. As for your second statement (the variable carry should appear in your invariant), let me think about how am I going to approach the problem through that. For time being it would be good if someone could help me figure it out as I'd spent long hours with no progress. Jun 25, 2017 at 12:55
• @caramel1995: The value of "carry" at the beginning of each iteration influences the result, so there should be something about "carry" in your loop invariant. If "carry" wasn't needed to be in the loop invariant, then you could replace it with some random value and the algorithm would still work. Which is unlikely to be correct. Jun 25, 2017 at 14:55

Step 1: Fix the typo in c[i=]. That's obviously wrong. (Done).

Step 1a: Try what happens when your algorithm adds 11 and 01. Notice that the result is wrong.

Step 1b: Fix the bug in your code. Check what happens in your algorithm again.

Step 2: Write down what is true at the end of the function which proves that the code is correct.

Step 3: Write down what is correct after the last iteration where i = 1, before setting C [1] = carry, which will lead to the statement in Step 2.

Step 4: Write down what is correct after each loop iteration, for each value of i.

Step 5: Write down what must be true before each loop iteration to get the result in Step 4.

Step 6: Figure out how Step 4 leads to Step 5.

Step 7: Check that Step 5 is true before the first iteration.

Pseudocode:

ADD-BINARY(A,B)

carry = 0

for i = length[A] to 1
C[i+1] = ( A[i] + B[i] + carry ) % 2
carry  = ( A[i] + B[i] + carry ) / 2

C[1] = carry


Loop invariant :

Concatenating carry and C[ i+2, i+3, i+4......] gives the binary sum of A[ i+1, i+2, i+3.........] and B[ i+1, i+2, i+3...........].

Before the first iteration it says that carry and c[n+2] is sum of A[n+1] and B[n+1]. Now A,B and C have invalid array index, so the statement should hold true.

After first iteration (i=n) it says the same as above. After second iteration (i=n-1) it says carry and C[n+1] = A[n] + B[n] which is true and same is true for other values of i.

The loop terminates when i=0 and it fails the test i should be upto 1. Now it says that carry and C[2......n+1] = A[1.....n] + B[1.....n]. ( the value of C[1] is given by the carry.) This is also true and we have the required answer.