Consider the algorithm LastMatch below, which returns the offset (shift) of the last occurrence of the pattern P in text T, or -1 if P does not occur in T:
LastMatch(T,P) for(s = T.length - P.length downto 0) j = 1 while(j =< P.length and P[j] == T[s + j]) j++ if(j == P.length + 1) return s return -1
I've been given a loop invariant for the while loop:
$\forall k(1 \leq k<j \rightarrow P[k] ==T[s+k])$
The initialisation of this invariant confuses me. Before we enter the while loop, $j=1$. So we're asking is there a $1\leq k<1$ such that $P[k] ==T[s+k]$?
I cannot find a $k$ which satisfies this inequality, so I do not understand what this is saying. So why is the invariant satisfied before we enter the loop? Is it because when I cannot find a $k$ it implies that $P[k]$ and $T[s+k]$ are both equal to the empty set?