Confusione dell'inizializzazione invariante in loop

Question

Considera l'algoritmo Lastmatch di seguito, che restituisce l'offset (shift) dell'ultima occorrenza del modello P nel testo T o -1 se P non si verifica 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

Mi è stato dato un ciclo invariante per il ciclo:

$ forall k (1 leq k

L'inizializzazione di questa invariante mi confonde. Prima di inserire il ciclo while, $ j = 1 $. Quindi chiediamo che c'è un $ 1 leq k <1 $ tale che $ P [k] == t [s+k] $?

Non riesco a trovare un $ k $ Il che soddisfa questa disuguaglianza, quindi non capisco cosa sta dicendo. Allora perché l'invariante è soddisfatto prima di entrare nel ciclo? È perché quando non riesco a trovare un $ k $ implica questo $ P [k] $ e $ T [s+k] $ sono entrambi uguali al set vuoto?