Results 1 to 3 of 3

Math Help - Hoare Calculus

  1. #1
    Newbie
    Joined
    Jun 2013
    From
    budapest
    Posts
    1

    Hoare Calculus

    hello everyone,,i need help,, i have been trying to use a Hoare calculus for proving a program,, but i couldn't understand the Hoare rules please i need some one to solve and explain to me how to use the Hoare calculus for proving this :


    P = ( X, T[1],,T[n] , n < N )


    1. Y := 1
    2. Z := 0
    3. while ( Y ≤ n )
    4. if ( X = T[Y] ) then
    5. Z := Y
    6. endif
    7. Y := Y+1
    8. endwile

    Q = ( X = T[Z] ) OR ( Z = 0 )

    The invariant of the loop P = ( X = T[Z] ) OR ( Z = 0 )



    these are the steps that i have to used (decomposition steps, Hoare derivation steps, invariant finding, proof of steps.)

    thanks in advance have a good day
    Follow Math Help Forum on Facebook and Google+

  2. #2
    Senior Member
    Joined
    Feb 2013
    From
    Saudi Arabia
    Posts
    440
    Thanks
    86
    Follow Math Help Forum on Facebook and Google+

  3. #3
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,527
    Thanks
    773

    Re: Hoare Calculus

    Quote Originally Posted by Mehyar View Post
    i have been trying to use a Hoare calculus for proving a program,, but i couldn't understand the Hoare rules
    If you don't understand the rules, then you should start with that. Post specific questions that you have about inference rules of the Hoare logic.

    Quote Originally Posted by Mehyar View Post
    P = ( X, T[1],,T[n] , n < N )

    1. Y := 1
    2. Z := 0
    3. while ( Y ≤ n )
    4. if ( X = T[Y] ) then
    5. Z := Y
    6. endif
    7. Y := Y+1
    8. endwile

    Q = ( X = T[Z] ) OR ( Z = 0 )
    It is not clear to me what P is. The formula Q is a postcondition, but P does not look like a proposition.

    Explaining this derivation in full would be a little too much for one question. You should ask more specific questions or show some work. Basically, you need to write a proposition between every two lines of code. The one after line 1 can be (Y = 0), but it seems that the value of Y is irrelevant for the following, so it can be just True. The proposition after line 2 is (Z = 0). Then you can use the rule of consequence to change it to the invariant P' because (Z = 0) implies P'. The body of the loop needs more work.

    Edit: Questions about logic should be posted to the Discrete Math subforum.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Hoare Logic Problems
    Posted in the Discrete Math Forum
    Replies: 3
    Last Post: August 18th 2012, 11:57 AM
  2. Replies: 1
    Last Post: December 13th 2011, 09:11 PM
  3. Replies: 1
    Last Post: February 11th 2010, 07:09 AM
  4. Replies: 1
    Last Post: June 23rd 2008, 09:17 AM
  5. Replies: 1
    Last Post: June 7th 2008, 11:47 AM

Search Tags


/mathhelpforum @mathhelpforum