Proving correctness of an exponentiation routine

I have the following exponentiation routine, which takes $O(\log n)$ steps

function power(a:real, n:positive integer)
begin
x:=1;
i:=n;
while i > 0 do
begin
if(i % 2 == 1) then   //i odd
x:=x*a
i:=floor(i/2)
if(i > 0) then
a:=a*a
end;
power:=x
end

I'm trying to prove that it always gives $a^n$. I think it might be provable via induction on $n$. in the examples i went through i found that it always ends with $i=1$ before the final division down to $0$.

• So, what's the question? – Raphael May 24 '16 at 22:45
• @Raphael Seems clear to me: how to prove that the final value of a is $a^n$ where $a$ is the initial value of a. (The code is either missing var in front of a:real or should be a function that ends by returning a.) – Gilles May 24 '16 at 23:25
• @Gilles It's a problem dump with some narrative about an approach. Where exactly is miniparser stuck? What do they need to know? – Raphael May 24 '16 at 23:48
• @Raphael Presumably stuck trying induction on $n$, which isn't an easy approach here. miniparser, you want a loop invariant; proving it will involve recursion on $i$. – Gilles May 24 '16 at 23:56
• miniparser please state more clearly how your attempt failes or what do you expect. As Raphael stated there is no question, just statements what you are doing. @reuns your comment looks more like answer. – Evil May 25 '16 at 15:13

A standard approach to proving correctness of a program involving a loop is to use a loop invariant. Loop invariant $P(j)$ is a statement indexed by the iteration number $j$ (or a parameter related to the iteration number) that asserts a certain mathematical relationship between some variables appearing in your code. Proving $P(j)$ is true for all $j$ is typically done by induction. You show that $P(0)$ is true, i.e., the loop invariant is true prior to the beginning of the loop. You show that $P(i)$ is true implies $P(i+1)$ is true. Then you can conclude that the statement $P(n)$ (or $P(n+1)$) must be true, which asserts the relationship between the variables of interest that is directly relevant to the correctness of the algorithm. Note that if $j$ is some parameter related to the iteration number (e.g., $j$ could be $n$ minus the iteration number), the starting point and the direction of the induction might be different. Finding the right loop invariant is usually the hardest part.
Let's find a loop invariant for your code. Note that you overwrite the variable $a$ inside the loop. This means that I cannot use $a$ in the loop invariant to refer to the original input, but I'd like to. Therefore I introduce a new letter $\alpha$ to refer to the value of $a$ that is passed to the function, i.e., the first input. The rest of the variables are exactly as in your code. Our loop invariant $P(i)$ will be indexed by the variable $i$, which is related to the iteration number, but starts with $n$ and decreases to $0$ similar to what I wrote about above. Define the following loop invariant: $$P(i) \text{ is true if and only if } x*a^i == \alpha^n$$ Clearly, at the beginning you have $x=1$, $a=\alpha$, and $i = n$, so $P(n)$ is true. I leave proving the inductive step to you (note you will be proving $P(n)$ is true implies $P(\lfloor n/2 \rfloor)$ is true, so this induction skips over lots of values, but it's okay - why?). When the algorithm terminates you have $P(0)$, which asserts $x*a^0 = \alpha^n$, i.e., $x = \alpha^n$, which is what you needed to prove.
• it's ok for the induction to skip over values of $n$ because the induction is on the number of times the loop executes. – miniparser Jun 21 '16 at 13:20