loop invariants the final justification technique we discuss in this section is the loop invariant to prove some statement about loop is correctdefine in terms of series of smaller statements lk where the initial claiml is true before the loop begins if - is true before iteration jthen will be true after iteration the final statementlk implies the desired statement to be true let us give simple example of using loop-invariant argument to justify the correctness of an algorithm in particularwe use loop invariant to justify that the functionfind (see code fragment )finds the smallest index at which element val occurs in sequence def find(sval) """return index such that [ =valor - if no such element "" len( = while if [ =val return match was found at index + return - code fragment algorithm for finding the first index at which given element occurs in python list to show that find is correctwe inductively define series of statementsl that lead to the correctness of our algorithm specificallywe claim the following is true at the beginning of iteration of the while loopl val is not equal to any of the first elements of this claim is true at the beginning of the first iteration of the loopbecause is and there are no elements among the first in (this kind of trivially true claim is said to hold vacuouslyin iteration jwe compare element val to element sjand return the index if these two elements are equivalentwhich is clearly correct and completes the algorithm in this case if the two elements val and sjare not equalthen we have found one more element not equal to val and we increment the index thusthe claim will be true for this new value of jhenceit is true at the beginning of the next iteration if the while loop terminates without ever returning an index in sthen we have that isln is true--there are no elements of equal to val thereforethe algorithm correctly returns - to indicate that val is not in