# Loop invariant for

The programme returns the number of digits of an integer $n>0$. I still have some difficulties to understand the difference between the loop invariant condition and what the loop should actually does. Clearly, we loop until the number is greater than 0. Is this the loop invariant condition? I know that by definition, the loop invariant should be true before, during and after the loop. At each iteration $j\geq 1$ we check the number $\frac{n}{j*10}\geq 1$ and if so we increment $length$, otherwise we stop and we print it. Thanks for your clarifications.

static void Main()
{

int length = 1, n;
Console.Write("Input the number n");
n = Convert.ToInt32(Console.ReadLine());

//pre-condition: length=1 and n>0
//loop invariant: ?
while ((n /= 10) >= 1)
{
length++;
}
//post-condition: length=number of digits of n
Console.WriteLine("The number of digits of integer n is " + length);
}

• The stated post condition does not hold in general: at the end of the loop $n$ is zero, while length can be anything, not the length of $0$. The length is the number of digits $n$ had before the loop started. The specification, as stated, is wrong. – chi Mar 10 '18 at 21:52
• @chi could you please give me an hint on how to get to the right condition? I tried also to think backwards, i.e. knowing our post-condition "number of digits of n", yet I can only think of the while condition $n=n/10 \geq 1$ – FunnyBuzer Mar 12 '18 at 10:13
• Usually one start with a precondition n=N>0 with N denoting a constant value, rather than a program variable. At the end you have as a post condition something like length = number of digits of N (instead of n) – chi Mar 12 '18 at 11:02