1. ## loop invariant

q)use loop invariant to prove that the following program segment for computing the nth power wher n is positive intger of a real number x is correct
power:=1
i:=1
whlie i<=n
begin
power:=powe*x
i:=i+1
end
solution:
i try to solve as follows please tell if i am right or wrong
the precondition:
we assume that p is positive integer which is true so our precondition is true
loop invariant s(n): powern =powern + x
in = in +1
is this true for all n>=0?
s(0)when the loop is not yet been executed

power0=power0 + x
i0 = i0+1
which means that s(0) is true
-> we assume that s(k) for some k>=0 which means that
powerk = powerk + x
ik = ik+1
->after one more pass throgh the loop
powerk+1=powerk+1+ x
ik+1 = ik+1 +1
this s(k+1) which is true
For the loop we now know
s(0) is true
s(k) ->s(k+1) is true
this means that s(n) is true for all n>=0
for all n>=0 the loop invariant is true
powern =powern + x
in = in +1
the loop terminate when i>n and reach the power
->at loop termination we got the power
so the post condition is true
so our program segment works

2. ## Re: loop invariant

First, write code segments between the [code]...[/code] tags. They preserve consecutive spaces and alignment, which is lost in regular text.

Originally Posted by annie12
Code:
power:=1
i:=1
while i<=n
begin
power:=power*x
i:=i+1
end
Originally Posted by annie12
the precondition:
we assume that p is positive integer which is true so our precondition is true
Neither p nor the precondition were defined, so this sentence does not make sense.

Originally Posted by annie12
loop invariant s(n): powern =powern + x
in = in +1
I don't know what you mean by power and i with subscripts. Also, a loop invariant should be a logical statement, not a piece of code, in particular, not an assignment. An assignment like "power = power + x" may make sense in a program, but as a logical statement, it is always false unless x = 0. Finally, I don't understand why you are talking about "power + x" since it never occurs in the program, unlike "power * x". Your version of the invariant looks nothing like "power = xⁿ", which is what needs to be proved eventually. So, the rest of the reasoning does not make sense to me.

A loop invariant is a logical statement that uses program variables (especially those that are changed during loop execution). It should be true immediately before the loop, and if it is true before execution of the loop body, it should stay true after the execution. In this case, the invariant together with ¬(i ≤ n) (the negation of the loop guard, which is true after the loop has finished) must imply that power = xⁿ.

Suppose that x = 2. Let's write the values of i and power before the loop and after successive executions of the loop body.
Code:
                                i  power
before the loop  1    1
after 1  execution of the body  2    2
after 2 executions of the body  3    4
after 3 executions of the body  4    8
after 4 executions of the body  5    16
Can you come up with a logical formula that relates i, power and x (= 2)?

3. ## Re: loop invariant

so i can prove it as follows
let p(s) be a loop invariant which which we apply on a variable x to find its power
when s=0 ,then power is equal to one so p(0) holds so our loop invariant is true before execution
when s=k we got power until our conter reach upto k
so post conditions are true because s(k) is true after loop terminated
so our program segments work

4. ## Re: loop invariant

Sorry, this still does not make any sense.

Originally Posted by annie12
so i can prove it as follows
let p(s) be a loop invariant which which we apply on a variable x to find its power
Which loop invariant? You can't prove something until you formulate exactly what you are proving. That's why I suggested in post #2 finding a relationship between i, x and power. It must be a concrete logical formula, such as "ix = power" (this one does not work).

Originally Posted by annie12
when s=k we got power until our conter reach upto k
What does it mean, "we got power"?

5. ## Re: loop invariant

so which thing we are indicating to loop invariant,can power=i^x is loop invariant i dont inderstand,its confusing

6. ## Re: loop invariant

First, you need to make sure that you intuitively understand why the code is correct. It works because the loop is executed n times, and each time power (whose initial value is 1) is multiplied by x. So, the final value of power is xn.

A loop invariant is like a path connecting the initial values of the variables involved in the loop, i.e., x, n, i and power, with their final values. It is some property P(x, n, i, power) that is true before the loop started, after the loop has finished, and also after each iteration. A useful loop invariant is a generalization of the final property: power = xn (since this is what we are interested in) that is true not only after the end of the loop, but also while it is running. By generalization I mean that P(x, n, i, power) should imply power = xn for the final values of the variables.

I asked you two times to look at the table of values of i and power (since x and n don't change) in post #2 and come up with a property that is always true for them. You seemed to ignore this advice, and I don't know how to avoid this step. Assume that x = 2 and n = 10. Here are two properties that don't work:

power = xn

and

power = ix.

Substitute the values of x = 2, n = 10, as well as i and power from the table to convince yourself that they don't indeed work. Next, come up with some similar property P(x, n, i, power) that does work for the values in that table.

7. ## Re: loop invariant

let p be the loop invariant involving power=x^i-1 and i<=n+1
p is true before the loop starts because now power=x^1-1=x^0=1 and i=0+1=1
p is true during loop executionb because now power=x^i-1*x =x^i and i<=n
p is true when loop is terminated because now power=x^n and i<=n+1

8. ## Re: loop invariant

Originally Posted by annie12
let p be the loop invariant involving power=x^i-1 and i<=n+1
Excellent! Except instead of "Let p be ... involving ..." I would write "Let p be the property saying..." or "Let p(x, n, i, power) be power=x^(i-1) and i <= n + 1". The word "involving" is not precise. Also, it is important to put parentheses around i-1 because exponentiation has a higher precedence than subtraction, so x^i-1 means (x^i) - 1.

Originally Posted by annie12
p is true before the loop starts because now power=x^1-1=x^0=1 and i=0+1=1
Concerning i, we have i = 1, so i <= n + 1 because by assumption n is a positive integer, i.e., 1 <= n.

Originally Posted by annie12
p is true during loop executionb because now power=x^i-1*x =x^i and i<=n
Here you need to consider two states of the program: before and after execution of the loop body, and prove that if p is true in the first state, then it is true in the second one. Suppose that power = x^(i-1) and i <= n + 1 and that the loop guard, i.e., i <= n, are true before execution of the loop body. Then after execution, the new value of power is power' = power * x, and the new value of i is i' = i + 1. Therefore,

power' = power * x = x^(i-1) * x = x^(i-1+1) = x^(i+1-1) = x^(l'-1),

so p holds of power' and i' instead of power and i, as required. Concerning the second condition in p, i.e., i <= n + 1, it follows from the loop guard since i <= n implies that i' = i + 1 <= n + 1.

Originally Posted by annie12
p is true when loop is terminated because now power=x^n and i<=n+1
We don't use the fact that power=x^n to conclude that p is true when the loop is terminated; it is the other way around. We assume that the loop terminated; therefore, the guard condition: i <= n, is false, i.e., i > n is true. Since we proved that the invariant holds before the loop and is preserved by the execution of the body, we also know that it holds after the loop finishes. Therefore, we know that power = x^(i-1), i <= n + 1 and i > n. The last two statements imply that i = n + 1, so power = x^(i-1) = x^n, which is what we were after the whole time.