# Hoare Calculus

• Jun 1st 2013, 05:44 AM
Mehyar
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
• Jun 1st 2013, 11:04 AM
MINOANMAN
Re: Hoare Calculus
• Jun 1st 2013, 11:57 AM
emakarov
Re: Hoare Calculus
Quote:

Originally Posted by Mehyar
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
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.