Proof by Induction of Pseudo Code

Question

I don't really understand how one uses proof by induction on psuedocode. It doesn't seem to work the same way as using it on mathematical equations.

I'm trying to count the number of integers that are divisible by k in an array.

Algorithm: divisibleByK (a, k)
Input: array a of n size, number to be divisible by k
Output: number of numbers divisible by k

int count = 0;
for i <- 0 to n do
    if (check(a[i],k) = true)
        count = count + 1
return count;


Algorithm: Check (a[i], k)
Input: specific number in array a,  number to be divisible by k
Output: boolean of true or false

if(a[i] % k == 0) then
    return true;
else    
    return false;

How would one prove that this is correct? Thanks

Answer 1

In this case I would interpret "inductively" as "induction over the number of iterations".

To do this we first establish a so called loop-invariant. In this case the loop invariant is:

             count stores the number of numbers divisible by k with index lower than i.

This invariant holds upon loop-entry, and ensures that after the loop (when i = n) count holds the number of values divisible by k in whole array.

The induction looks like this:

1. Base case: The loop invariant holds upon loop entry (after 0 iterations)

   Since i equals 0, no elements have index lower than i. Therefore no elements with index less than i are divisible by k. Thus, since count equals 0 the invariant holds.

2. Induction hypothesis: We assume that the invariant holds at the top of the loop.

3. Inductive step: We show that the invariant holds at the bottom of the loop body.

   After the body has been executed, i has been incremented by one. For the loop invariant to hold at the end of the loop, count must have been adjusted accordingly.

   Since there is now one more element (a[i]) which has an index less than (the new) i, count should have been incremented by one if (and only if) a[i] is divisible by k, which is precisely what the if-statement ensures.

   Thus the loop invariant holds also after the body has been executed.

Qed.

---

In Hoare-logic it's proved (formally) like this (rewriting it as a while-loop for clarity):

{ I }
{ I[0 / i] }
i = 0
{ I }
while (i < n)
    { I ∧ i < n }
    if (check(a[i], k) = true)
        { I[i + 1 / i] ∧ check(a[i], k) = true }
        { I[i + 1 / i][count + 1 / count] }
        count = count + 1
        { I[i + 1 / i] }
    { I[i + 1 / i] }
    i = i + 1
    { I }
{ I ∧ i ≮ n }
{ count = ∑ 0 x < n;  1 if a[x] ∣ k, 0 otherwise. }

Where I (the invariant) is:

     count = ∑_{x < i} 1 if a[x]∣k, 0 otherwise.

(For any two consecutive assertion lines ({...}) there is a proof-obligation (first assertion must imply the next) which I leave as an exercise for the reader ;-)