# Can we ignore the postcondition in the Hoare conditional rule when there is a return statement?

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?

• AFAIK (standard) Hoare logic only directly "supports" a very basic programming language whose statements are either assignments, conditionals, or while-loops. Hence, if there is a return statement, then its meaning in Hoare logic must be specified somewhere (i.e., through an axiom); either that or you'll have to translate your code to apply Hoare logic on it. A return is equivalent to an assignment plus a "break" statement, which, in turn, can be expressed as a loop condition; try rewriting your pseudocode with that in mind. – dkaeae Mar 18 '19 at 14:22