Proof by Induction of Pseudo Code

问题:

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

回答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 ;-)

回答2:

We prove correctness by induction on n, the number of elements in the array. Your range is wrong, it should either be 0 to n-1 or 1 to n, but not 0 to n. We'll assume 1 to n.

In the case of n=0 (base case), we simply go through the algorithm manually. The counter is initiated with value 0, the loop doesn't iterate, and we return the value of counter, which as we said, was 0. That's correct.

We can do a second base case (although it's unnecessary, just like in regular maths). n=1. The counter is initialised with 0. The loop makes one pass, in which i takes value 1, and we increment counter iff the first value in a is divisible by k (which is true because of the obvious correctness of the Check algorithm).
Therefore we return 0 if a[1] was not divisible by k, and otherwise we return 1. This case also works out.

The induction is simple. We assume correctness for n-1 and will prove for n (again, just like in regular maths). To be properly formal, we note that counter holds the correct value that we return by the end of the last iteration in the loop.

By our assumption, we know that after n-1 iterations counter holds the correct value regarding the first n-1 values in the array. We invoke the base case of n=1 to prove that it will add 1 to this value iff the last element is divisible by k, and therefore the final value will be the correct value for n.

QED.

You just have to know what variable to perform the induction on. Usually the input size is most helpful. Also, sometimes you need to assume correctness for all naturals less than n, sometimes just n-1. Again, just like regular maths.