Prove using induction that the loop invariant holds

Question

//Precondition: n > 0
//Postcondition: returns the minimum number of decial digits
//               necessary to write out the number n

 int countDigits(int n){
1.    int d = 0;
2.    int val = n;
3.    while(val != 0){
4.        val = val / 10;     // In C++: 5 / 2 === 2
5.        d++;
6.    }
7.    return d;
}

Invariant: Just before evaluating the loop guard on line 3, n with its rightmost d digits removed is identical to val. (Assume that the number 0 takes 0 digits to write out and is the only number that takes 0 digits to write out).

Prove using induction that the loop invariant holds.

Now I've always thought that proof with induction is assuming that by replacing a variable within an equation with k will be true then I must prove k+1 will also be true. But I'm not really given an equation in this question and just a block of code. Here's my base case:

Just before evaluating the loop guard on line 3, d is equal to 0 and on line 2, val == n, so if n has its rightmost 0 digit removed, it is val. Therefore, the base case holds.

I'm not really sure how to write the inductive step after this since I'm not sure how to prove k+1..

Note that you do not necessarily have to do induction over one of the variables; have you considered induction over the length of n? — Joost

jods jods · Accepted Answer · 2014-04-24T23:40:24

The logic is really the same as with an equation, except you replace the k value in your equation by the n iteration of the loop:

base case is that the loop invariant holds before starting the loop;
you have to prove that if the invariant holds before iteration N, it will still hold after execution of iteration N.

From 1. and 2. we conclude by induction that the invariant holds at the end of the loop (or at the end of any iteration, in fact).

EDIT and this is interesting because the loop ends with val == 0. Your invariant (still true at the end of the loop) is n with its rightmost d digits removed is identical to val, so n with d digits removed is identical to 0 at this point, so d is correctly the number of digits required to display n.

Prove using induction that the loop invariant holds

1 Answers