I'm proving the correctness of naive string matching using Hoare logic. I have the following pseudocode:
NaiveStringMatch(T,P)
<precondition: T is an array of n > 0 characters
P is an array of m > 0 characters>
for(s = 0 to T.length - P.length)
<invariant: forall 0 ≤ s’ < s there is no match>
j = 1
while(j ≤ P.length and P[j] == T[s + j])
<invariant: P[1 … j] matches T[s ... s + j]>
j++
if(j == P.length + 1)
return s
return -1
<postcondition: if s > -1 then P[i] == T[i + s], 1 ≤ i ≤ m,
and there is no s' < s for which this holds>
The thing I am struggling with is the conditional statement
if(j == P.length + 1)
return s
In particular, the Hoare logic proof rule for conditionals, and the required postcondition, $\psi$, in this case. The conditional rule looks like this:
$$\frac{\{\phi \wedge B\}C_1 \{\psi\} \>\>\>\>\> \{\phi \wedge \neg B\}C_2 \{\psi\}} {\{\phi\} \>\> if \>\> B \>\> then \>\> C_1 \>\> else \>\> C_2 \>\> \{\psi\}}$$
My precondition, $\phi$, is this: $$\phi = \text{for all shifts } 0 \leq s' < s \text{ there is no match, and } \\ P[1...j] \text{ match the corresponding characters in } T[s...s + j]$$
The postcondition, $\psi$, that I have been given is this:
$$\psi = \text{for all shifts } 0 \leq s' \leq s \text{ there is no match}$$
Looking a bit closer, we notice that when the inner loop terminates, then j ≤ P.length + 1. There are two cases:
1) if j < P.length + 1, then P does not match T at shift s, so the outer for loop invariant is maintained. After evaluating the if statement, we also satisfy $\psi$, since there is no match when $s' = s$.
2) if j == P.length + 1, P does match T at shift s, and the algorithm terminates, returning s. So the outer for loop invariant is maintained. Now this is where I am confused. After evaluating the if statement, how is $\psi$ satisfied here? Because after the if statement is executed, clearly we can find the shift $s' = s$ for which there is a valid match. So in my mind $\psi$ is not satisfied. Unless the return statement means we do not need to check $\psi$ and therefore we just ignore the fact that $\psi$ is not satisfied?
