Results 1 to 7 of 7

Math Help - Wrong Invariant?

  1. #1
    Newbie
    Joined
    Aug 2012
    From
    China
    Posts
    18

    Wrong Invariant?

    Hi, I am working through Hoare Logic problem, I think my invariant is wrong but I cannot think of the good invariant.. please help me with this.

    The program:

    {n >= 0}

    x := 0;
    t := 0;
    while ( x < n ) do
    x := x+1;
    t := t+x;
    {t = (n^2 + n) / 2}

    My invariant was (t = (x^2 +x ) / 2) but it seems that it is wrong
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Sep 2012
    From
    Australia
    Posts
    3,668
    Thanks
    609

    Re: Wrong Invariant?

    Hey gomdohri.

    Can you explain in simple terms what the invariant corresponds to (for someone that is not familiar with the terminology in Hoare logic)?
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Newbie
    Joined
    Aug 2012
    From
    China
    Posts
    18

    Re: Wrong Invariant?

    Extremely simple invariant - something that never changes so here I am looking for the good loop invariant
    Follow Math Help Forum on Facebook and Google+

  4. #4
    MHF Contributor
    Joined
    Sep 2012
    From
    Australia
    Posts
    3,668
    Thanks
    609

    Re: Wrong Invariant?

    Are you talking about in the loop (where you want t to be a function of x explicitly) for each iteration of t?

    If that is the case then I agree with you on the formula you have. Did you try and test it within your code (by using a print statement)?
    Follow Math Help Forum on Facebook and Google+

  5. #5
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,539
    Thanks
    778

    Re: Wrong Invariant?

    Quote Originally Posted by gomdohri View Post
    My invariant was (t = (x^2 +x ) / 2) but it seems that it is wrong
    I think the invariant is correct. Why do you think it is wrong? The only problem is that it does not allow proving that t = (n^2 + n) / 2 after the loop. The Hoare logic rule for while is

    Code:
           {P /\ B} S {P}
    -------------------------------
    {P} while B do S done {~B /\ P}
    So, with the invariant t = (x^2 + x) / 2 we can only conclude that x >= n /\ t = (x^2 + x) / 2; we can't conclude that x = n. Can you think of how to change the invariant to be able to deduce x = n after the loop?

    By the way, you should indicate somehow that the body of the loop consists of two assignments (e.g., by placing "done" or "end" after the body of the loop).
    Follow Math Help Forum on Facebook and Google+

  6. #6
    Newbie
    Joined
    Aug 2012
    From
    China
    Posts
    18

    Re: Wrong Invariant?

    Sorry for the confusion here yes, the problem with my invariant is that I cannot prove that t = (n^2 + n) /2 after the loop so that is why I had to change the invariant. However, since I am not really familiar with Hoare logic, I could not think of the invariant that also proves t = (n^2 + n) / 2
    Follow Math Help Forum on Facebook and Google+

  7. #7
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,539
    Thanks
    778

    Re: Wrong Invariant?

    The part of the invariant you are missing is not related to t. Basically, you need to deduce the following.

    Code:
    {x <= n}
    
    while (x < n) do
      x := x+1;
    done;
    
    {x = n}
    The rule for while allows you to conclude that the loop guard (i.e., x < n) is false after the end of the loop, so you know that x >= n after the loop. You also need to know that x <= n. What should the invariant for the program above be?
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. T-invariant subspace
    Posted in the Advanced Algebra Forum
    Replies: 1
    Last Post: October 25th 2010, 06:45 AM
  2. another T-invariant question
    Posted in the Advanced Algebra Forum
    Replies: 1
    Last Post: November 12th 2009, 11:43 AM
  3. T-invariant
    Posted in the Advanced Algebra Forum
    Replies: 1
    Last Post: September 17th 2009, 10:32 PM
  4. Replies: 6
    Last Post: August 12th 2009, 02:15 AM
  5. help me on invariant subspace please
    Posted in the Advanced Algebra Forum
    Replies: 2
    Last Post: January 7th 2009, 07:57 AM

Search Tags


/mathhelpforum @mathhelpforum