Introduction: Developing and understanding loops
We introduce a methodology for understanding and also developing loops. It is based on the ideas of program correctness presented earlier. In fact, we present a systematic way to prove while-loops and for-loops correct. This methodology is practical, and we will use it to study several searching and sorting algorithms. Even later, we use the methodology to present algorithms, like finding the shortest path in a graph —used by google maps and many other apps to find a route to drive from one place to another. Without the methodology, presenting, understanding and implementing such algorithms is much harder.
Why learn about loop invariants and loop correctness?
Alex Fusco tells you why this material is important. He shows you an algorithm that you can't understand without this material, and discusses an important engineering principle. (4 minutes) Read it here: why study loops?.pdf
The loop invariant and four loopy questions
Using a flow chart for a loop, Alex Fusco explains what a loop invariant is. He introduces four questions about loops whose answers determine whether a loop is correct or not. (4.5 minutes) Read it here: the loop invariant.pdf
Here's an annotated while loop, with initialization:
// {Q}
init
// invariant: P
while (B) S
// {R}
Here are the four loopy questions. We suggest that you memorize them:
- 1. How does it start: Is {Q} init {P} true?
- 2. How does it end: Is P && !B => R true?
- 3. Does the repetend make progress toward termination?
- 4. Does the repetend maintain P: Is {P && B} S {P} true?
Answering the four loopy questions
The previous video discussed the four loopy questions, using a particular loop. Annika Lutan investigates the four loopy questions for this loop in detail, showing that all four questions can be answered "yes", thus proving that the loop (with initialization) is correct.. (5.2 minutes) Read it here: example1.pdf
Developing a loop using the four loopy questions
Annika Lutan shows you second example to show how a loop can be developed using the four loopy questions. This is far more important than just using them to check a given loop. Mastering this material will allow you to "know" many algorithms important algorithms, not because you memorize code but because you can develop them whenever you want, using the methodology. These algoriths become memorable. (5.6 minutes) Read it here: example2.pdf