2. Practice on developing parts of loops

This material may seem foreign at first, difficult, confusing. That's because it goes against the way you have been thinking about programming ever since you started to program. That's ok.

The way to change how you think about loops to use the new methodology is to practice. On this web page, we present examples and exercises that give you such practice. First, we deal with the first loopy question. Then the second loopy question. Finally, the third and fourth loopy questions together. Giving examples and exercises dealing with one loopy question at a time will let you focus on that loopy question, in a way that you can't when you are thinking about a whole loop.

Our focus here is on the development of the parts of a loop.

First loopy question: Does it start right?

The first loopy question is: Does it start right: Is {Q} init {P} true? Alex Fusco gives some examples and some exercises. The exercises are short! Do them! (5 minutes) Read it here: DoesItStartRight?.pdf

In this short video, Annika Lutan video deals with the first loopy question when assertions are give as array diagrams. The exercises are short! Do them!(3.25 minutes) Read it here: Does it start right?.pdf

Second loopy question: Does it end right?

The second loopy question is: Does it end right: Is P && !B => R true? Here's the neat thing about using the method to determine when a loop should stop: You don't have to count how many iterations the loop should make and use that count as the stopping value. So, you can expect to make fewer "off by one" errors. Annika Lutan gives you some examples and some exercises. The exercises are short! Do them! (3.5 minutes) Read it here: Does it end right?.pdf

Alex Fusco shows you how to answer the second loopy question when assertions are given by array diagrams. The exercises are short! Do them! (3 minutes) Read it here: Does it end right?.pdf

Third and fourth loopy questions: Does the repetend do what it is supposed to do?

We work with the third and fourth loopy question together, because they are related. Together, the must endure that the repetend makes progress toward termination and keeps the invariant true.

In order to answer whether the repetend makes progress toard termination, we need to know what that means. Generallly, this can be indicated by some expression whose value must get closer to 0, and when te loop terminates, that expression's value wil be 0. We'll make this clear in our examples.

Another point. The first question when dealing with the repetend must be: How does it make progress toward termination. If instead we used the question about keeping the invariant true, we would answer: "don't do anything", because the invariant is already true when the repetend starts.

The third and fourth loop questions are:
Does the repetend make progress toward termination?
Does the repetend keep P true: Is {Q && B} S {P} true?

Alex Fusco shows you how to handle these two questions together, because they often have to be answered together. (4.25 minutes) Read it here: Is the repetend right?.pdf
Note: video has a typo in Exercise 2. P: v = minimum of b[k..n] should be P: v = minimum of b[0..k]. It's correct in the script.

Annika Lutan shows you how to answer the third and fourth loopy questions when assertions are given by array diagrams.Do the exercises! (3.5 minutes) Read it here: Is the repetend right?.pdf