(Readings, CSC 207 2013F)

Loop invariants provide an invaluable tool not only for helping ensure the correctness of your code, but also for thinking about the structure of code in the first place. We introduce the basics of loop invariants and consider both textual and visual invariants.

Introduction

Experience shows that as programmers develop more complicated iterative algorithms, they tend to make subtle mistakes in their design that are hard to fix. (Yes, programmers also make mistakes in their recursive designs.) As you begin to develop more complicated algorithms, you will find that a variety of tools can help you better ensure that these algorithms are correct. You've already seen one kind of tool - a systematic test suite can help you identify potential errors.

Loop invariants provide an equally important starting point - instead of having you reflect upon incorrect code, loop invariant help you develop correct code from the start. Basically, a loop invariant is a (formal) statement about the state of your program.

Citations

This reading was inspired, in part, by Henry Walker's two short articles on loop invariants.

Jon Bentley's reading on binary search remains my primary inspiration for encouraging my students to think about loop invariants.

Jon Bentley. 1983. Programming pearls: Writing correct programs. Commun. ACM 26, 12 (December 1983), 1040-1045. DOI=10.1145/358476.358484 http://doi.acm.org/10.1145/358476.358484.