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); 
        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?

  • $\begingroup$ 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? $\endgroup$ – chi Apr 24 '18 at 12:25
  • $\begingroup$ @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. $\endgroup$ – FunnyBuzer Apr 24 '18 at 12:43
  • $\begingroup$ Something looks wrong: if both are multiplications, reverse(n,0) = 0 * .... = 0 $\endgroup$ – chi Apr 24 '18 at 14:09
  • $\begingroup$ @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? $\endgroup$ – FunnyBuzer Apr 24 '18 at 18:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.