proof - Prove using induction that the loop invariant holds -

//precondition: n > 0 //postcondition: returns minimum number of decial digits //               necessary write out 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: before evaluating loop guard on line 3, n rightmost d digits removed identical val. (assume number 0 takes 0 digits write out , number takes 0 digits write out).

prove using induction loop invariant holds.

now i've thought proof induction assuming replacing variable within equation k true must prove k+1 true. i'm not given equation in question , block of code. here's base case:

just before evaluating loop guard on line 3, d equal 0 , on line 2, val == n, if n has rightmost 0 digit removed, val. therefore, base case holds.

i'm not sure how write inductive step after since i'm not sure how prove k+1..

the logic same equation, except replace k value in equation n iteration of loop:

1. base case loop invariant holds before starting loop;
2. you have prove if invariant holds before iteration n, still hold after execution of iteration n.

from 1. , 2. conclude induction invariant holds @ end of loop (or @ end of iteration, in fact).

edit , interesting because loop ends val == 0. invariant (still true @ end of loop) n rightmost d digits removed identical val, n d digits removed identical 0 @ point, d correctly number of digits required display n.