# Proof of correctness recursive reverse digit function

This is an attempt to understand better recursion. The following recursive function returns the integer obtained by reversing the digits of an input integer. I'm trying to prove its correctness:

public static int reverse(int n)
{
return reverse(n, 0);
}
public static int reverse(int number, int reverted)
{
if (number!=0)
return reverse(number/10, reverted*10 + number % 10);
else
return reverted;
}


The program requires the integer input to be strictly positive, and the program clearly terminates because n is decreasing. Moreover, we have the relation

reverse(xy, z) = z*reverse(xy) = z*reverse(y)*reverse(x)


How should I proceed to complete a formal proof of correctness for recursion?

• What does z*reverse(y)·reverse(x) mean? I guess one symbol is multiplication: which one? what is the other one? Is xy assumed to stand for a 2 digit number, or what, precisely? – chi Apr 24 '18 at 12:25
• @chi Sorry, it's both multiplications, I corrected it. xy is an integer made of two integers, e.g. 1234 where x=12 and y=34. I still don't see how one can prove recursion. In iteration there's the concept of loop invariant, by this can clearly not be used in the case of recursion. – FunnyBuzer Apr 24 '18 at 12:43
• Something looks wrong: if both are multiplications, reverse(n,0) = 0 * .... = 0 – chi Apr 24 '18 at 14:09
• @chi sure you are right. Multiplication doesn't make sense. Just starting from an example, by calling the function reverse(12,34)=34·reverse(12)=3421. From this observation, could you please suggest a way to conclude the proof? – FunnyBuzer Apr 24 '18 at 18:41