4
$\begingroup$

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?

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

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$.

$\endgroup$
  • $\begingroup$ oh okay so power = x^i is the invariant? $\endgroup$ – Jack Mar 22 '16 at 17:43
  • 2
    $\begingroup$ Yes, that works. $\endgroup$ – Yuval Filmus Mar 22 '16 at 17:44
  • $\begingroup$ @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. $\endgroup$ – Musa Al-hassy Apr 7 '16 at 16:47
  • $\begingroup$ @MusaAl-hassy You can reformulate the program so that initially $i=0$, and the loop increments $i$ at each iteration. Then everything works. $\endgroup$ – Yuval Filmus Apr 7 '16 at 16:50
  • $\begingroup$ yup; I've done that below :-) $\endgroup$ – Musa Al-hassy Apr 9 '16 at 15:17
1
$\begingroup$

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!

$\endgroup$
  • 1
    $\begingroup$ 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). $\endgroup$ – Raphael Apr 7 '16 at 20:06
  • $\begingroup$ I look forwards to it! ^_^ $\endgroup$ – Musa Al-hassy Apr 9 '16 at 15:16
0
$\begingroup$

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

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

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.