I tried making an example of loop invariant.

What's this?

• I researched the definition of the "loop invariant", by studying Introduction to algorithms.
• I became interested in some examples of that.

What I learned

Definition of the "loop invariant"

Because there is no definition of the loop invariant in Introduction to Algorithms, I'll use this definition in another university.

A loop invariant is a condition that is true at the beginning and end of every iteration of a loop.

written in

CS 2112/ENGRD 2112 Fall 2020

Three things we need to show when using loop invariant

We should show these three things when expressing why an algorithm is correct.

1. Initialization: a condition is true before the first iteration of the loop
2. Maintenance: If a condition is true before an iteration of the loop, it remains true before the next iteration
3. Termination: The loop terminates. Additionally, a condition gives us useful properties that help show the algorithm is correct.

side note

However, I haven't understood whether these things are necessary to define loop invariant.

For example, k==1 fills the definition of the loop invariant in this code.

• This is a condition.
• This is true at the beginning and end of every iteration(Of course!).

So, we can call it a loop invariant, can't it?

k = 1

for i in range(10):
  assert k == 1 # => (pass)

This point is discussed also in the stack overflow, and I found its definition fuzzy.

stackoverflow.com

But for now, I'll use a condition that fills those three things because something that doesn't fill them seems unnecessary.

An example of loop invariants

I try to think about the problem that I seek for the minimum number of the given list.

In this problem, I can say "minimum of the sublist(l[:i]) is m" is a loop invariant.

Let's see the required things in order.

1.Before the first iteration of the loop, i = 1.(According to Introduction to Algorithms, I first set loop variable). As you know, at this time m = l[0], so explicitly min(l[:1]) is m.

2.Given min(l[:k]) = m, if l[k] is less than m, then m = l[k] and min(l[:k + 1]) = m. This shows the second requirement is filled.

3.I assume the loop variable is incremented when the loop is terminated. In this case min(l[:i + 1]) is m. This shows that the minimum number of the list is m.

l = [2, 4, 1, 5, 3]

m = l[0]

for i in range(1, len(l)):
  assert min(l[:i]) == m
  if l[i] < m:
    m = l[i]

print(m) # => 1