Loop Invariants Are Necessary for Writing Proper Loops

Contrary to my piece from a couple years ago, I'm actually coming out in favor of incorporating loop invariants in computer science education—albeit with more of a focus on reasoning than formal verification. A Little History Previously, I wrote a piece titled, "No One Uses Loop Invariants: Just Ask Google." As the title states, I presented the idea that we might not need to teach loop invariants so formally. After all, we teach them at the very end of the first course in our software sequence, and students always joke about how that "information was useless." Seeing their frustration, I ended up writing a somewhat tongue-in-cheek piece denouncing the teaching of loop invariants. Interestingly, I ended up getting an email from a professor in Dijkstra's orbit (yes, that Dijkstra). As they put it, Dijkstra was their doctor grandfather, which is actually verifiable through the Mathematics Genealogy Project. Though, you'll have to take my word for it. Anyway, they took issue with the premise of my work. Specifically, they stated: I want to share with you my take on the matter, get your (perhaps) countervailing opinion, and possibly convince you to write a follow-up piece that takes the opposite point of view from the one conveyed in your first piece by such phrases as "no one uses loop invariants" and "I don’t think loop invariants have a place in broader computer science education". My position is: "Everyone uses loop invariants" and "Loop invariants have a place in computer science education starting in CS1". Having discussed with them a bit, I'm more than comfortable to provide a bit more clarity on my position. Reframing My Position Prior to our email exchange, I had not considered the idea that loop invariants could have utility beyond provability (i.e., formal program verification). As a result, my main criticism of loop invariants was that they're taught formally as a mechanism for provability. After all, that's how we teach them at my university. Specifically, we introduce loop invariants in two lectures at the end of our CS1 (or really CS1.5) course. We do not give students the tools to craft their own loop invariants, but we do expect them to be able to read and reason about loop invariants. For example, it's common to ask students on the final to predict the result of a handful of variables given a loop invariant and a loop without its body. As it turns out, loop invariants aren't only necessary for proving correctness of software. They're also necessary for writing proper loops. I was partially convinced of this framing when loop invariants were presented to me as a reasoning mechanism. Here, you can see me initially buying into the idea during our exchange: Therefore, if the argument is that loop invariants are necessary from a reasoning standpoint, I buy that logic and would even be willing to write a follow up piece advocating for that position (for the record, I have written a pair of articles showing how my views changed on software testing). In fact, I would agree that it would be beneficial to discuss loop invariants (maybe not so formally) with students as early as possible (i.e., CS1). Perhaps my original take is a bit misguided in that I personally don't need explicit loop invariants to reason about loops, but students do (akin to understanding arithmetic BEFORE using a calculator). However, what really sold me was their response to the previous paragraph: Should I read "I personally don't need explicit loop invariants to reason about loops" with an emphasis on "explicit"? Should assume you are saying something like: "Loop Invariants are so baked into my way of thinking about iteration that I don't even need to write them out explicitly (with or without formality) to develop and reason about a loop". In other words, the reason I am so comfortable with casting loop invariants aside is because I've internalized them. In contrast, students who have not internalized the concept of a loop invariant are destined to write bad loops. Hitting the Educational Angle Given that loop invariants serve not only the provability of software but also the reasoning of it, I have to walk back my previous statement about no one using them: everyone does, though mostly implicitly. Without loop invariants, we might instinctively be able to identify a bad loop, but we can't really explain why. Therefore, we might talk about code "smells" or simply outright ban certain practices like using break and continue. Instead, it would be better to build up the concept of iteration with loop invariants in mind. In my own experience, I've often been able to condense student loops without really having the language to explain why I'm able to do that. I usually use a phrase like, "move all the logic you need to break the loop into the loop condition," which cuts down on a lot of branching. Now, I think it's more useful to ask students what they expect the program state to look like in the middle of a loop. Likewise, how do they expect the state to be the same (i.e., the loop invariant) and different (i.e., the loop variant) one iteration before and after? In other words, loop invariants are the core of how iteration works. If they can make sense of this, then they can write a proper loop. With that said, I'm satisfied with this more disciplined understanding of looping. Often, I am critical of some of the advice you might get about "the right way" to write code, but this is one of those times where the mindset is grounded in more than vibes. As a result, next time you write a loop, think about the big picture: what is meant to remain constant? In the next section, I'll give a quick example using a problem we do in our own classes. Loop Invariants in Practice One of the more famous problems in our software sequence is given the name nextWordOrSeparator. The premise is pretty straightforward: write a method that takes a string, an index, and a set of separators and returns the next word or separator in the string. For those of you with some programming background, you probably already know what this method is meant to do: tokenization. Of course, we introduce this method far before students have a concept of tokenization. Otherwise, we'd deal with the headache of students trying to reinvent tokenization. Anyway, take a moment to think about how you'd implement this method. To help, here's the method header (it's Java, but you can treat it like pseudocode): private static String nextWordOrSeparator( String text, int position, Set separators ) {} Now, clearly there is a loop involved in this process. We need to iterate from the starting position to some unknown ending position. For starters, what kind of loop works best when we don't know when to stop? While we can surely make a variety of loop constructs work, there is really only one loop for this job: a while loop. The reason being that a while loop is also known as an indefinite loop, and we use them in scenarios when we don't know when to stop. With that said, it might be tempting to select a for-loop or even a for-each-loop, as we've probably used them on strings in the past. After all, it's really easy to iterate over all of the indices with a for-loop or all of the characters with a for-each-loop. In this case, because we don't know when to stop the loop, a while loop is the better choice. Now, suppose we're given the following arguments: "how now brown cow", 0, {" "}. We know by looking at these inputs that we're starting at the beginning of the string, and that there are three separators in our string (i.e., the three spaces). Mentally, we know we just need to make it to the first space and return "how". Intuitively, the algorithm for getting the next word or the next separator seems pretty straightforward, yet students really struggle to write the code for it. I think what trips them up is that they imagine all these edge case scenarios. For example, they know that the character at the starting position could be a word character or a separator character, so they envision a branch. Likewise, they think they need to build up an output string while carefully paying attention to the type of character they append, which results in additional branches. The reality is that we just need to zoom out and consider the loop invariant. In this case, the string and its length never change. The separators never change. The only thing that's changing is the index. Therefore, our loop invariant states that everything from the starting position to the current index must be the same class of thing (i.e., a part of a word or a part of a separator). Within that framework, the solution is really as simple as testing for two things: 1) we don't run off the end of the string and 2) the current character is the same class of thing as the starting character. If either of these conditions fail, we return the substring from the starting position to the current index. It might look something like this in pseudocode: private static String nextWordOrSeparator(...) { isSeparator = text[position] in separators i = position while (i < text.length and isSeparator == text[i] in separators) { i++; } return text[position, i]; } Typically, even the cleanest solutions I've seen from students use two identical loops separated by a branch (i.e., use one loop when the starting character is a separator and use the other when its not). Even then, students will still keep a simple boundary check in their loop condition and rely on break or return to exit when they hit a bad character. Other students will try to build the string as they go, which results in other painful issues related to branching, especially if their code includes the previous issues. All of that is to say that the usual way of constructing a loop without the internalized idea of a loop invariant leads to patchwork solutions. Rather than zooming out and trying to figure out if your solution makes sense, a lot of folks get in the habit of bug squashing. They think their solution is so close and just one more change will do it. In reality, the code becomes a jumbled mess that could be simplified. It's why I often have students rewrite their code after drawing some diagrams rather than trying to fix their existing solution. Discipline Makes You a Better Developer I have been teaching software development for close to a decade at this point, and I have often worried about the way that modern software development tools actually hurt learning. For example, I've probably mentioned it a few times, but it's always painful to watch students navigate even syntax errors by mindlessly modifying their code until the red squiggly line goes away. Now, with the prevalence of generative AI, I worry that students aren't going to understand anything at all. In the past, while I've resisted some of the more theoretical elements of our field, I'm starting to see the value in helping students understand the theoretical underpinnings of software development. Furthermore, I see value in following a software development discipline or set of principles—lest we become glorified button pushers. Anyway, that's about all I wanted to cover on the topic. As a goofy aside, this article is perhaps timely because I was just covering structured programming, a term created by Dijkstra, in my new "Dark Arts" series. Specifically, I introduce Java's labeled statements feature and how it's related to the "goto" statement. It's a short read, so why not check it out? As always, if you enjoyed this, feel free to check out some of these other related pieces: A Case Study on the Philosophy of Software Design The Problem Enums Are Intended to Solve Trust Me! Your Code Isn’t That Bad Otherwise, consider checking out my list of ways to grow the site. If not, see you next time!