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 )

- Y := 1
- Z := 0
- while ( Y ≤ n )
- if ( X = T[Y] ) then
- Z := Y
- endif
- Y := Y+1
- 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