Results 1 to 8 of 8
Like Tree3Thanks
  • 1 Post By emakarov
  • 1 Post By emakarov
  • 1 Post By emakarov

Math Help - loop invariant

  1. #1
    Newbie
    Joined
    Aug 2013
    From
    pakistan
    Posts
    22

    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
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,504
    Thanks
    765

    Re: loop invariant

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

    Quote Originally Posted by annie12 View Post
    Code:
    power:=1
    i:=1
    while i<=n
    begin
        power:=power*x
        i:=i+1
    end
    Quote Originally Posted by annie12 View Post
    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.

    Quote Originally Posted by annie12 View Post
    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)?
    Thanks from annie12
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Newbie
    Joined
    Aug 2013
    From
    pakistan
    Posts
    22

    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
    Follow Math Help Forum on Facebook and Google+

  4. #4
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,504
    Thanks
    765

    Re: loop invariant

    Sorry, this still does not make any sense.

    Quote Originally Posted by annie12 View Post
    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).

    Quote Originally Posted by annie12 View Post
    when s=k we got power until our conter reach upto k
    What does it mean, "we got power"?
    Follow Math Help Forum on Facebook and Google+

  5. #5
    Newbie
    Joined
    Aug 2013
    From
    pakistan
    Posts
    22

    Re: loop invariant

    so which thing we are indicating to loop invariant,can power=i^x is loop invariant i dont inderstand,its confusing
    Follow Math Help Forum on Facebook and Google+

  6. #6
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,504
    Thanks
    765

    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.
    Thanks from annie12
    Follow Math Help Forum on Facebook and Google+

  7. #7
    Newbie
    Joined
    Aug 2013
    From
    pakistan
    Posts
    22

    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
    Follow Math Help Forum on Facebook and Google+

  8. #8
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,504
    Thanks
    765

    Re: loop invariant

    Quote Originally Posted by annie12 View Post
    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.

    Quote Originally Posted by annie12 View Post
    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.

    Quote Originally Posted by annie12 View Post
    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.

    Quote Originally Posted by annie12 View Post
    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.
    Thanks from annie12
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Inner Loop of a limacon
    Posted in the Trigonometry Forum
    Replies: 1
    Last Post: November 25th 2012, 07:18 PM
  2. Number Loop
    Posted in the Advanced Statistics Forum
    Replies: 3
    Last Post: October 31st 2012, 05:59 PM
  3. Using a for loop and while loop.
    Posted in the Math Software Forum
    Replies: 1
    Last Post: April 19th 2010, 01:18 PM
  4. Loop Statements
    Posted in the Math Topics Forum
    Replies: 3
    Last Post: April 9th 2009, 05:29 AM
  5. Matlab While Loop Help
    Posted in the Math Software Forum
    Replies: 1
    Last Post: March 8th 2009, 07:50 PM

Search Tags


/mathhelpforum @mathhelpforum