Midnote: 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.
Lisa Lippincott designed the software architectures of Tanium and BigFix, two systems for managing large fleets of computers. She's currently assistant chair of the numerics study group of the C++ standardization committee. In her spare time, she studies mathematical logic, and wants to make computer-checked proofs of correctness a routine part of programming.