I'm proving the correctness of naive string matching using Hoare logic. I have the following pseudocode:

        <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]>
           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?

  • 1
    $\begingroup$ 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. $\endgroup$
    – dkaeae
    Mar 18, 2019 at 14:22


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.