will now store the comparison pointthe variable will as before point to the corresponding element of the pattern see fig - string pattern - fig in the notations of the kmp algorithmthe alignment position of the pattern is now - (and not ias was the case with the simple algorithmthe central pont of the algorithm is the comparison of [iand [ ]if they are equal then and are both increased by otherwise the pattern must be shifted by assigning to of some smaller value the boundary case shows that one should provide for shift of the pattern entirely beyond the current comparison point (so that [ becomes aligned with [ + ]for thisit is convenient to choose - the main loop of the algorithm takes the following formi : : while ( ( (( or ( [ip[ ])do inci )incj elsif ( ( [ip[ ]* : end this formulation is admittedly not quite completebecause it contains an unspecified shift value we shall return to it shortlybut first point out that the invariant here is chosen the same as in the simple algorithmin the new notation it is ( -jp( -jjthe post condition of the loop -evaluated as conjuction of negations of all guards -is given by the expression ( >mor ( > )but in reality only equalities can occur if the algorithm terminates due to mthe term ( -jjof the invariant implies ( -mmr( )that isa match at position - otherwise it terminates with nand since mthe first term of the invariantq( - )implies that no match exists at all we must now demonstrate that the algorithm never falsifies the invariant it is easy to show that it is established at the beginning with the values let us first investigate the effect of the two statements incrementing and by in the first branch they apparently do not falsify ( - )since the difference - remains unchanged nor do they falsify ( -jjthanks to the equality in the guard (see the definition of pas to the second branchwe shall simply postuate that the value always be such that replacing by will maintain the invariant provided that the assignment : represents shift of the pattern to the right by - positions naturallywe wish this shift to be as large as possiblei to be as small as possible this is illustrated by fig string pattern = = fig assignment : shifts pattern by - positions =