Why Loops End

When we write a loop in a program, we usually intend that each execution of the loop will eventually end. To meet that intention, we should understand the reasons why loops end, and, to give others confidence in our code, we should learn to communicate those reasons.

In this talk, I will examine the reasons why loops end, and present a scheme for expressing those reasons formally within the source code of a program, in a lightly extended version of C++. Starting from procedural first principles of stability of objects, substitutability of values, and repeatability of operations, I will show how reasons for loops to end can be expressed directly by the program’s flow of execution within the neighborhood of the loop.