How would I find the loop invariant for this small body of code?

Question

Pre-condition: list of ints where len(list) >= 2

Post-condition: return the second smallest value. If there exists two smallest values in list, return smallest.

def SecondSmallest(list):
1   smallest = min(list[0], list[1])
2   second_smallest = max(list[0], list[1])
3   i = 2
4   while i < len(list):
5       item = list[i]
6       if item < second_smallest:
7           if item < smallest:
8               second_smallest = smallest
9               smallest = item
10          else:
11              second_smallest = item
12      i += 1
13  return second_smallest

Many Thanks.

Answer 1

A loop invariant is a predicate that holds for every iteration of the loop. See What is a loop invariant? for more details.

In your specific case, for every iteration, 1 < i < len(list) holds.

For a more formal definition, see: https://en.wikipedia.org/wiki/Loop_invariant