Results 1 to 4 of 4

Math Help - Hoare Logic Problems

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

    Hoare Logic Problems

    Hi, I have started studying Hoare Logic but I have two questions and I hope that you can help me with this.

    First question is about Loops

    ^ = powered by

    Prove {s = 2^i} while i < n do [i := i+1; s := s*2] {s = 2^i}

    I tried to find an invariant but failed.

    Second question is just about assignment statements but I am stuck

    this time /\ is 'and'

    Prove {(i = 5) /\ (a = 3)} a:= i +2 {a = 7}

    thank you!
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,513
    Thanks
    769

    Re: Hoare Logic Problems

    Code:
    ------------------------------------------------ Assignment
    {i = 5 /\ i + 2 = 7} a := i + 2 {i = 5 /\ a = 7}
    ------------------------------------------------ Consequence
         {i = 5 /\ a = 3} a := i + 2 {a = 7}
    I'll look at the loop later.
    Follow Math Help Forum on Facebook and Google+

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

    Re: Hoare Logic Problems

    for the first question, I 've learnt in a class that you should always start proving backwards, which means that I should replace the existing precondition with the postcondition first and in fact that's how I proved
    {i = 5} a := i+2 {(a = 7) /\ (i=5)} (this was the first question for the tutorial and the above was the second question for the tutorial). Is it really okay to start from the precondition?

    second I don't understand the assignment part ,

    how can you direct change the postcondition a = 7 to (i = 5 /\ a = 7)?
    Follow Math Help Forum on Facebook and Google+

  4. #4
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,513
    Thanks
    769

    Re: Hoare Logic Problems

    Quote Originally Posted by gomdohri View Post
    Prove {s = 2^i} while i < n do [i := i+1; s := s*2] {s = 2^i}

    I tried to find an invariant but failed.
    s = 2^i is the invariant.

    Quote Originally Posted by gomdohri View Post
    for the first question, I 've learnt in a class that you should always start proving backwards, which means that I should replace the existing precondition with the postcondition first and in fact that's how I proved
    {i = 5} a := i+2 {(a = 7) /\ (i=5)} (this was the first question for the tutorial and the above was the second question for the tutorial). Is it really okay to start from the precondition?
    It is indeed possible to take a piece of code with a given postcondition and invariants for each loop and construct the weakest precondition for this piece of code. If another precondition is given, you can verify if it implies the found weakest precondition and thus determine if it is sufficient to guarantee the given final postcondition. However, you can construct a derivation in any way that is convenient.

    Quote Originally Posted by gomdohri View Post
    second I don't understand the assignment part ,

    how can you direct change the postcondition a = 7 to (i = 5 /\ a = 7)?
    Do you have a problem with the consequence rule or with the assignment rule? The consequence rule works because i = 5 /\ a = 7 implies a = 7 (with regard to the postcondition) and i = 5 /\ a = 3 implies i = 5 /\ i + 2 = 7 (with regard to the precondition).

    In the following code I used rule from the Wikipedia article about Hoare logic.

    Code:
    ------------------------------------ Ass-t
    {2s = 2^(i+1)} i := i + 1 {2s = 2^i}
    ------------------------------------ Cons ----------------------------- Ass-t
      {s = 2^i} i := i + 1 {2s = 2^i}         {2s = 2^i} s := 2*s {s = 2^i}
      --------------------------------------------------------------------- Comp-n
                    {s = 2^i} i := i + 1; s = 2*s {s = 2^i}
                 ------------------------------------------------ Cons
                 {s = 2^i /\ i < n} i := i + 1; s = 2*s {s = 2^i}
          ----------------------------------------------------------------- While
          {s = 2^i} while i < n [i := i + 1; s = 2*s] {s = 2^i /\ ~(i < n)}
          ----------------------------------------------------------------- Cons
               {s = 2^i} while i < n [i := i + 1; s = 2*s] {s = 2^i}
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. logic problems
    Posted in the Discrete Math Forum
    Replies: 3
    Last Post: August 2nd 2011, 01:07 PM
  2. Replies: 7
    Last Post: October 30th 2010, 02:55 PM
  3. Logic problems
    Posted in the Discrete Math Forum
    Replies: 5
    Last Post: May 11th 2010, 04:07 AM
  4. Logic problems?
    Posted in the Pre-Calculus Forum
    Replies: 1
    Last Post: May 12th 2009, 06:29 PM
  5. Logic Word Problems-need a faster method!
    Posted in the Algebra Forum
    Replies: 1
    Last Post: December 4th 2008, 10:34 PM

Search Tags


/mathhelpforum @mathhelpforum