# Finding a good loop invariant for a powering procedure

Consider the following algorithm for computing integer powers:

Procedure power(integer x, integer n)
power := 1
for i := 1 to n
power := power * x
return power


Can we say that the loop invariant is $power \leq x^n$ ?
Before the loop $power$ is initialized to $1$ so its equal to $1 \leq x^n$.

How do we prove maintenance of the invariant?

• Why do you think that the power can be greater then $x^n$?
– 3SAT
Mar 22 '16 at 16:40
• for first iteration could it be?
– Jack
Mar 22 '16 at 17:10

No, you can't say that $power \leq x^n$ is a loop invariant, since it is not maintained by the loop. For example, if $x > 1$ and at the current iteration $power = x^n$, then the invariant is satisfied at the beginning of the loop but not at the end of the loop.

Also, this loop invariant doesn't help you prove that at the end $power = x^n$, which is presumably your end goal.

Try to think of an invariant which describes the value of $power$ in terms of $x$ and $i$.

• oh okay so power = x^i is the invariant?
– Jack
Mar 22 '16 at 17:43
• Yes, that works. Mar 22 '16 at 17:44
• @YuvalFilmus mentions to consider the maintenance of the invariant but one must not forget the initialisation of the invariant. In particular, the invariant must be true before the loop even begins. In this case, it does not hold initially since $power = 1 \neq x^1 = x^i$. As such the mentioned candidate cannot be an invariant. One might argue that we're talking about $i$ before it even comes into scope and that itself is already dangerous, perhaps that's why Hoare logic tends to use the more general while-loop construct as it is clearer in such instances. Apr 7 '16 at 16:47
• @MusaAl-hassy You can reformulate the program so that initially $i=0$, and the loop increments $i$ at each iteration. Then everything works. Apr 7 '16 at 16:50
• yup; I've done that below :-) Apr 9 '16 at 15:17

Let's rewrite your code using a while-loop so that everything is explicit.

{ 1 ≤ n }
i ≔ 0; p ≔ 1;
while i < n:
i  ≔ i + 1; p  ≔ p * x
{ p ≈ xⁿ }


Note that the initialization sets i to 0 instead of 1!

Now after the loop is finished we will know that necessairly n < i and thattogether with whatever the invaraint is, call it I, we can establish the post-condition:

  n ≤ i ∧ I ⇒ p ≈ xⁿ
⇐⟨ arthimetic ; assuming i ≤ n ⟩
n ≤ i ≤ n ∧ I ⇒ p * xⁿ⁻ⁱ ≈ xⁿ
⇐⟨ one possible solution ⟩
I ≡ (i ≤ n ∧ p * xⁿ⁻ⁱ ≈ xⁿ)


Half of this is the invariant as mentioned in other answers, but ours is different in that it is particular to the while-loop setting with i begun at 0. Also, this is the full invariant, while others only mentioned half of it. The p * xⁿ⁻ⁱ ≈ xⁿ part can be simplified to p ≈ xⁱ but notice that we "calculated" I from what we know about the post-condition and the loop-guard! Moreover, the formulation found above leads to a nifty intutive interpretation:

    (product so far) * (product remaining) ≈ total product


Anyhow, we've chosen as invariant

I : i ≤ n ∧ p ≈ xⁱ


For it to be an invaraint, it must be initaly true before the loop begins:

  { 1 ≤ n } i ≔ 1; p ≔ x { I }
≡⟨ assignment rule ⟩
{ 1 ≤ n } i ≔ 1 { I[ p / x] }
≡⟨ substitution ⟩
{ 1 ≤ n } i ≔ 1 { i ≤ n ∧ x ≈ xⁱ }
≡⟨ assignment rule ⟩
1 ≤ n ⇒ 1 ≤ n ∧ x ≈ x¹ }
≡⟨ arithmetic ⟩
true


Also it must be maintained by the loop body,

   {I ∧ i < n} i  ≔ i + 1; p  ≔ p * x {I}
≡⟨ assignment rule, twice ⟩
I ∧ i < n ⇒ I[ p * x / p] [i+1 / i]
≡⟨ definitions and substitution ⟩
i ≤ n ∧ p ≈ xⁱ  ∧ i < n ⇒ i+1 ≤ n ∧ p * x ≈ xⁱ⁺¹
≡⟨ arithmetic: i < n ⇒ i+1 ≤ n and p ≈ xⁱ ⇒ p*x ≈ xⁱ⁺¹ ⟩
true


Sweet! However, we've only proven "partial correctness". To show total correctness we need to prove that the loop termiantes. That is we need a bound function bf that is intially positive and is decreased by the loop-body. Since the loop guard is i < n we may choose

  bf : n - i


and the loop guard ensures that it is initally positive: i < n ⇒ 0 < n - i ⇒ 0 < bf It remains to show that the loop-body decreases it: for any t, we must show

   { bf = t } i  ≔ i + 1; p  ≔ p * x { bf < t }
≡⟨ assignment rule, twice ⟩
bf = t ⇒ (bf < t)[ p*x / p] [i+1 / i]
≡⟨ defintions and substitution ⟩
n - i = t ⇒ n - (i + 1) < t
≡⟨ arithmetic ⟩
n - i = t ⇒ n - i - 1 < t
≡⟨ arithemtic ⟩
true


Sweet; that was fun!

Best of luck!

• I see you have been putting quite some effort into some answers. I don't have the time right now, but I hope that somebody will read and upvote them (or offer constructive criticism).
– Raphael
Apr 7 '16 at 20:06
• I look forwards to it! ^_^ Apr 9 '16 at 15:16

$$power = x^i$$is the invariant

• And how did you get this? Why should we believe it's true?
– Raphael
Apr 7 '16 at 20:05