Thread: Hoare Calculus

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

2. Re: Hoare Calculus

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.

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.