while ( ( [js[ + ]do inc(jendreturn ~( mend let the result be the index iwhich points to the first occurrence of match of the pattern within the string then (ishould hold in additionr(kmust be false for all denote the latter condition as ( ) (iak < ~ (kwith the problem thus formulateda linear search suggests itself (see sec ) : (adens _straight *while ( < - ~ (ido inc(iend the invariant of this loop is ( )which holds both before the instruction inc(iand -thanks to the second operand of the guard -after it an advantage of this algorithm is the transparency of its logicthe two loops are completely decoupled and one is hidden inside the function-procedure howeverthis same property may also be disadvantagefirstlythe additional procedure call at each step of potentially long loop may be too costly in such basic operation as the string search secondlythe more sophisticated algorithms considered in subsequent sections make use of the information obtained in the inner loop in order to increase in the external loop by value larger than so that the two loops are no longer independent one could eliminate the procedure by introducing logical variable to store its result and by embedding the loop from in the body of the main loop over howeverthe interaction of two loops via logical variable looses the original transparencywhich may cause errors in the program evolution formulation of such loops is facilitated by the so-called dijkstra loopwhich is multibranch version of the while loop with each branch having its own guard (see appendix cin the present case the two branches correspond to the steps in and jrespectively recall fig and introduce the predicate (ijthat expresses the match of the first characters of the pattern with the characters of the text starting from position ip(ijak < si+ pk then (ip(imfig shows that the current search state is characterized by and the invariant ( the condition that holds after each increase of or jcan be chosen as followsin the positions below there is no matchand in the position there is match of the first characters of the pattern this is formally expressed as followsq(ip(ijevidentlyj would mean there is required math of the entire pattern in the position iwhereas would mean that the text contains no match at all it is then sufficient to try to increment by in order to increase the matching segmentand if that is impossibleto move the pattern into new position by incrementing by and setting to in order to restart verifying the match from the beginning of the patterni : : while the matching segment can be increased do incj elsif the pattern can be moved do inci ) : end it remains to consider each step separately and to accurately formulate the conditions for which each step