How to write correct loops?

Question

Most of time while writing loops I usually write wrong boundary conditions(eg: wrong outcome) or my assumptions about loop terminations are wrong(eg: infinitely running loop). Although I got my assumptions correct after some trial and error but I got too frustrated because of the lack of correct computing model in my head.

/**
 * Inserts the given value in proper position in the sorted subarray i.e. 
 * array[0...rightIndex] is the sorted subarray, on inserting a new value 
 * our new sorted subarray becomes array[0...rightIndex+1].
 * @param array The whole array whose initial elements [0...rightIndex] are 
 * sorted.
 * @param rightIndex The index till which sub array is sorted.
 * @param value The value to be inserted into sorted sub array.
 */
function insert(array, rightIndex, value) {
    for(var j = rightIndex; j >= 0 && array[j] > value; j--) {
        array[j + 1] = array[j];
    }   
    array[j + 1] = value; 
};

The mistakes that I did initially were:

1. Instead of j >= 0 I kept it j > 0.
2. Got confused whether array[j+1] = value or array[j] = value.

What are tools/mental models to avoid such mistakes?

Answer 1

Test

No, seriously, test.

I've been coding for over 20 years and I still don't trust myself to write a loop correctly the first time. I write and run tests that prove it works before I suspect it works. Test each side of every boundary condition. For example a rightIndex of 0 should do what? How about -1?

Keep it simple

If others can't see what it does at a glance you're making it too hard. Please feel free to ignore performance if it means you can write something easy to understand. Only make it faster in the unlikely event that you really need to. And even then only once you're absolutely sure you know exactly what is slowing you down. If you can achieve an actual Big O improvement this activity may not be pointless, but even then, make your code as readable as possible.

Off by one

Know the difference between counting your fingers and counting the spaces between your fingers. Sometimes the spaces are what is actually important. Don't let your fingers distract you. Know whether your thumb is a finger. Know whether the gap between your pinky and thumb counts as a space.

Comments

Before you get lost in the code try to say what you mean in English. State your expectations clearly. Don't explain how the code works. Explain why you're having it do what it does. Keep implementation details out of it. It should be possible to refactor the code without needing to change the comment.

The best comment is a good name.

If you can say everything you need to say with a good name, DON'T say it again with a comment.

Abstractions

Objects, functions, arrays, and variables are all abstractions that are only as good as the names they are given. Give them names that ensure when people look inside them they won't be surprised by what they find.

Short names

Use short names for short lived things. i is a fine name for an index in a nice tight loop in a small scope that makes it's meaning obvious. If i lives long enough to get spread out over line after line with other ideas and names that can be confused with i then it's time to give i a nice long explanatory name.

Long names

Never shorten a name simply due to line length considerations. Find another way to lay out your code.

Whitespace

Defects love to hide in unreadable code. If your language lets you choose your indentation style at least be consistent. Don't make your code look like a stream of word wrapped noise. Code should look like it's marching in formation.

Loop constructs

Learn and review the loop structures in your language. Watching a debugger highlight a for(;;) loop can be very instructive. Learn all the forms: while, do while, while(true), for each. Use the simplest one you can get away with. Look up priming the pump. Learn what break and continue do if you have them. Know the difference between c++ and ++c. Don't be afraid to return early as long as you always close everything that needs closing. Finally blocks or preferably something that marks it for automatic closing when you open it: Using statement / Try with Resources.

Loop alternatives

Let something else do the looping if you can. It's easier on the eyes and already debugged. These come in many forms: collections or streams that allow map(), reduce(), foreach(), and other such methods that apply a lambda. Look for specialty functions like Arrays.fill(). There is also recursion but only expect that to make things easy in special cases. Generally don't use recursion until you see what the alternative would look like. If someone tells you tail recursion will magically keep you from blowing the stack then first check if your language optimizes tail recursion. Not all of them do.

Oh, and test.

Test, test, test.

Did I mention testing?

There was one more thing. Can't remember. Started with a T...

Answer 2

When programming it is useful to think of:

• pre-conditions
• post-conditions
• variants
• and invariants (of loops or types)

and when exploring uncharted territory (such as juggling with indices) it can be very, very, useful to not just think about those but actually make them explicit in the code with assertions.

Let's take your original code:

/**
 * Inserts the given value in proper position in the sorted subarray i.e. 
 * array[0...rightIndex] is the sorted subarray, on inserting a new value 
 * our new sorted subarray becomes array[0...rightIndex+1].
 * @param array The whole array whose initial elements [0...rightIndex] are 
 * sorted.
 * @param rightIndex The index till which sub array is sorted.
 * @param value The value to be inserted into sorted sub array.
 */
function insert(array, rightIndex, value) {
    for(var j = rightIndex; j >= 0 && array[j] > value; j--) {
        array[j + 1] = array[j];
    }   
    array[j + 1] = value; 
};

And check what we have:

• pre-condition: array[0..rightIndex] is sorted
• post-condition: array[0..rightIndex+1] is sorted
• invariant: 0 <= j <= rightIndex but it seems redundant a bit; or as @Jules noted in the comments, at the end of a "round", for n in [j, rightIndex+1] => array[j] > value.
• invariant: at the end of a "round", array[0..rightIndex+1] is sorted

So you can first write a is_sorted function as well as a min function working on an array slice, and then assert away:

function insert(array, rightIndex, value) {
    assert(is_sorted(array[0..rightIndex]));

    for(var j = rightIndex; j >= 0 && array[j] > value; j--) {
        array[j + 1] = array[j];

        assert(min(array[j..rightIndex+1]) > value);
        assert(is_sorted(array[0..rightIndex+1]));
    }   
    array[j + 1] = value; 

    assert(is_sorted(array[0..rightIndex+1]));
};

There is also the fact that your loop condition is a bit complicated; you might want to make it easier on yourself by splitting things up:

function insert(array, rightIndex, value) {
    assert(is_sorted(array[0..rightIndex]));

    for (var j = rightIndex; j >= 0; j--) {
        if (array[j] <= value) { break; }

        array[j + 1] = array[j];

        assert(min(array[j..rightIndex+1]) > value);
        assert(is_sorted(array[0..rightIndex+1]));
    }   
    array[j + 1] = value; 

    assert(is_sorted(array[0..rightIndex+1]));
};

Now, the loop is straightforward (j goes from rightIndex to 0).

Finally, now this needs to be tested:

• think of boundary conditions (rightIndex == 0, rightIndex == array.size - 2)
• think of value being smaller than array[0] or larger than array[rightIndex]
• think of value being equal to array[0], array[rightIndex] or some middle index

Also, do not underestimate fuzzing. You have assertions in place to catch mistakes, so generate a random array and sort it using your method. If an assertion fires, you found a bug and can extend your test suite.

Answer 3

Use unit testing/TDD

If you really need to access sequences through a for loop, you can avoid the mistakes through unit testing, and especially test driven development.

Imagine you need to implement a method which takes the values which are superior to zero, in reverse order. What test cases could you think of?

1. A sequence contains one value which is superior to zero.

   Actual: [5]. Expected: [5].

   The most straightforward implementation which satisfies the requirements consists of simply returning the source sequence to the caller.

2. A sequence contains two values, both superior to zero.

   Actual: [5, 7]. Expected: [7, 5].

   Now, you cannot just return the sequence, but you should reverse it. Would you use a for (;;) loop, another language construct or a library method doesn't matter.

3. A sequence contains three values, one being zero.

   Actual: [5, 0, 7]. Expected: [7, 5].

   Now you should change the code to filter the values. Again, this could be expressed through an if statement or a call to your favorite framework method.

4. Depending on your algorithm (since this is white-box testing, the implementation matters), you may need to handle specifically the empty sequence [] → [] case, or maybe not. Or you may ensure that the edge case where all values are negative [-4, 0, -5, 0] → [] is handled correctly, or even that boundary negative values are: [6, 4, -1] → [4, 6]; [-1, 6, 4] → [4, 6]. In many cases, however, you'll only have the three tests described above: any additional test won't make you change your code, and so would be irrelevant.

Work at higher abstraction level

However, in many cases, you can avoid most of those errors by working at a higher abstraction level, using existent libraries/frameworks. Those libraries/frameworks make it possible to revert, sort, split and join the sequences, to insert or remove values in arrays or doubly-linked lists, etc.

Usually, foreach can be used instead of for, making boundary conditions checking irrelevant: the language does it for you. Some languages, such as Python, don't even have the for (;;) construct, but only for ... in ....

In C#, LINQ is particularly convenient when working with sequences.

var result = source.Skip(5).TakeWhile(c => c > 0);

is much more readable and less error prone compared to its for variant:

for (int i = 5; i < source.Length; i++)
{
    var value = source[i];
    if (value <= 0)
    {
        break;
    }

    yield return value;
}

Answer 4

I agree with other people who say test your code. However, it's also nice to get it right in the first place. I have a tendency to get boundary conditions wrong in many cases, so I've developed mental tricks to prevent such problems.

With a 0-indexed array, your normal conditions are going to be:

for (int i = 0; i < length; i++)

or

for (int i = length - 1; i >= 0; i--)

Those patterns should become second nature, your shouldn't have to think about those at all.

But not everything follows that exact pattern. So if you're not sure if you wrote it right, here's your next step:

Plug in values and evaluate the code in your own brain. Make it as simple to think about as you possible can. What happens if the relevant values are 0s? What happens if they are 1s?

for(var j = rightIndex; j >= 0 && array[j] > value; j--) {
    array[j + 1] = array[j];
}   
array[j + 1] = value;

In your example, you're not sure if it should be [j] = value or [j+1] = value. Time to start evaluating it manually:

What happens if you have an array length 0? The answer becomes obvious: rightIndex must be (length - 1) == -1, so j starts at -1, so to insert at index 0, you need to add 1.

So we've proved the final condition correct, but not the inside of the loop.

What happens if you have an array with 1 element, 10, and we try to insert a 5? With a single element, rightIndex should start at 0. So the first time through the loop, j = 0, so "0 >= 0 && 10 > 5". Since we want to insert the 5 at index 0, the 10 should get moved to index 1, so array[1] = array[0]. Since this happens when j is 0, array[j + 1] = array[j + 0].

If you try to imagine some large array and what happens inserting into some arbitrary location, your brain will probably get overwhelmed. But if you stick to simple 0/1/2 size examples, it should be easy to do a quick mental run through and see where your boundary conditions break down.

Imagine you never heard of the fence post problem before and I tell you I have 100 fence posts in a straight line, how many segments between them. If you try to imagine 100 fence posts in your head, you're just going to get overwhelmed. So what's the fewest fence posts to make a valid fence? You need 2 to make a fence, so imagine 2 posts, and the mental image of a single segment between the posts makes it very clear. You don't have to sit there counting posts and segments because your made the problem into something intuitively obvious to your brain.

Once you think it's correct, it's then good to run it through a test and make sure the computer does what you think it should, but at that point it should just be a formality.

Answer 5

Off-by-one errors are one of the most common programming mistakes. Even experienced developers get this wrong sometimes. Higher level languages usually have iteration constructs like foreach or map which avoids explicit indexing altogether. But sometimes you do need explicit indexing, as in your example.

The challenge is how to think of ranges of array cells. Without a clear mental model, it becomes confusing when to include or exclude the end points.

When describing array ranges, the convention is to include lower bound, exclude upper bound. For example the range 0..3 is the cells 0,1,2. This conventions is used throughout 0-indexed languages, for example the slice(start, end) method in JavaScript returns the subarray starting with index start up to but not including index end.

It is clearer when you think about range indexes as describing the edges between array cells. The below illustration is an array of length 9, and the numbers below the cells is aligned to the edges, and is what is used to describe array segments. E.g. it is clear from the illustration than the range 2..5 is the cells 2,3,4.

┌───┬───┬───┬───┬───┬───┬───┬───┬───┐
│ 0 │ 1 │ 2 │ 3 │ 4 │ 5 │ 6 │ 7 │ 8 │   -- cell indexes, e.g array[3]
└───┴───┴───┴───┴───┴───┴───┴───┴───┘
0   1   2   3   4   5   6   7   8   9   -- segment bounds, e.g. slice(2,5) 
        └───────────┘ 
          range 2..5

This model is consistent with having array length be the upper bound of an array. An array with length 5 have cells 0..5, which means there are the five cells 0,1,2,3,4. This also means the length of a segment is the higher bound minus the lower bound, i.e. the segment 2..5 has 5-2 = 3 cells.

Having this model in mind when iterating either upwards or downwards makes it a lot clearer when to include or exclude the end points. When iterating upwards you need to include the start point but exclude the end point. When iterating downwards you need to exclude the start point (the higher bound) but include the end point (the lower bound).

Since you are iterating downwards in your code, you need to include the low bound, 0, so you iterate while j >= 0.

Given this, your choice to have the rightIndex argument represent the last index in the subarray breaks the convention. It means you have to include both endpoints (0 and rightIndex) in the iteration. It also makes it difficult to represent the empty segment (which you need when you are starting the sort). You actually have to use -1 as rightIndex when inserting the first value. This seem pretty unnatural. It seem more natural to have rightIndex indicate the index after the segment, so 0 represent the empty segment.

Of course your code is extra confusing because it expands the sorted subarray with one, overwriting the item immediately after the initially sorted subarray. So you read from index j but writes the value to j+1. Here you should just be clear that j is the position in the initial subarray, before the insertion. When index operations gets too tricky it helps me to diagram it on a piece of grid paper.

Answer 6

I got too frustrated because of the lack of correct computing model in my head.

Is a very interesting point to this question and it generated this comment:-

There is only one way: understand your problem better. But that is as general as your question is. – Thomas Junk

...and Thomas is right. Not having a clear intent for a function should be a red-flag - a clear indication that you should immediately STOP, grab a pencil and paper, step away from the IDE, and break the problem down properly; or at very least sanity-check what you have done.

I've seen so many functions and classes that have become a complete mess because the authors have attempted to define the implementation before they have fully defined the problem. And it's so easy to deal with.

If you don't fully understand the problem then you're also unlikely to be coding the optimal solution (either in terms of efficiency or clarity), nor are you going to be able to create genuinely useful unit tests in a TDD methodology.

Take your code here as an example, it contains a number of potential flaws which you've not considered yet for example:-

• what if rightIndex is too low? (clue: it will involve data loss)
• what if rightIndex is outside the array bounds? (will you get an exception, or did you just create yourself a buffer overflow?)

There are a few other issues related to the performance and design of the code...

• will this code need to scale? Is keeping the array sorted the best option, or should you look at other options (like a linked-list?)
• can you be sure of your assumptions? (can you guarantee the array be sorted, and what if it isn't?)
• are you reinventing the wheel? Sorted arrays are a well-known problem, have you studied the existing solutions? Is there a solution already available in your language (such as SortedList<t> in C#)?
• should you be manually copying one array entry at a time? or does your language provide common functions like JScript's Array.Insert(...)? would this code be clearer?

There are plenty of ways this code could be improved but until you have properly defined what you need this code to do, you're not developing code, you're just hacking it together in the hope that it will work. Invest the time in it and your life will get easier.

Answer 7

The introduction to your question makes me think you haven't learned to code properly. Anyone who is programming in an imperative language for more than a few weeks should really be getting their loop bounds right first-time in more than 90% of cases. Perhaps you are rushing to start coding before you've thought through the problem sufficiently.

I suggest you correct this deficiency by (re-)learning how to write loops -- and I'd recommend a few hours working through a range of loops with paper and pencil. Take an afternoon off to do this. Then spend 45 min or so a day working on the topic until you really get it.

It's all very well testing, but you should be testing in the expectation that you generally get your loop bounds (and the rest of your code) right.

Answer 8

Perhaps I should put some flesh on my comment:

There is only one way: understand your problem better. But that is as general as your question is

Your point is

Although I got my assumptions correct after some trial and error but I got too frustrated because of the lack of correct computing model in my head.

When I read trial and error, my alarm bells start ringing. Of course many of us know the state of mind, when one wants to fix a small problem and has wrapped his head around other things and starts guessing in one or the other way, to make the code seem to do, what is supposed to do. Some hackish solutions come out of this - and some of them are pure genius; but to be honest: most of them are not. Me included, knowing this state.

Independendly from your concrete problem, you asked questions, about how to improve:

1) Test

That was said by others and I would have nothing valuable to add

2) Problem Analysis

It is hard to give some advice to that. There are only two hints I could give you, which probably help you improving your skills on that topic:

• the obvious and most trivial one is in the long term the most effective: solve many problems. While practicing and repeating you develop the mindset which helps you for future tasks. Programming is like any other activity to be improved by hard work practicing

Code Katas are a way, which might help a bit.

How do you get to be a great musician? It helps to know the theory, and to understand the mechanics of your instrument. It helps to have talent. But ultimately, greatness comes from practicing; applying the theory over and over again, using feedback to get better every time.

Code Kata

One site, which I like very much: Code Wars

Achieve mastery through challenge Improve your skills by training with others on real code challenges

They are relatively small problems, which help you sharpen your programming skills. And what I like most on Code Wars is, that you could compare your solution to one of others.

Or maybe, you should have a look at Exercism.io where you get feedback from the community.

• The other advice is nearly as trivial: Learn to break down problems You have to train yourself, breaking down problems into really small problems. If you say, you have problems in writing loops, you make the mistake, that you see the loop as a whole construct and do not deconstruct it into pieces. If you learn to take things apart step by step, you learn to avoid such mistakes.

I know - as I said above sometimes you are in such a state - that it is hard to break "simple" things into more "dead simple" tasks; but it helps a lot.

I remember, when I first learned professionally programming, I had huge problems with debugging my code. What was the problem? Hybris - The error can not be in such and such region of the code, because I know that it can not be. And in consequence? I skimmed through code instead of analyzing it I had to learn - even if it was tedious to break my code down instruction for instruction.

3) Develop a Toolbelt

Besides knowing your language and your tools - I know these are the shiny things of which developers think first - learn Algorithms (aka reading).

Here are two books to start with:

• Introduction into algortihms

• Algorithms

This is like learning some recipes to start off cooking. At first you don't know what to do, so you have to look, what prior chefs cooked for you. The same goes for algortihms. Algorithms are like cooking recipies for common meals (data structures, sorting, hashing etc.) If you know them (at least try to) by heart, you have a good starting point.

3a) Know programming constructs

This point is a derivative - so to say. Know your language - and better: know, what constructs are possible in your language.

A common point for bad or inefficent code is sometimes, that the programmer does not know the difference between different types of loops (for-, while- and do-loops). They are somehow all interchangeably useable; but in some circumstances choosing another looping construct leads to more elegant code.

And there is Duff's device ...

P.S.:

otherwise your comment is no good than Donal Trump.

Yes, we should make coding great again!

A new motto for Stackoverflow.

Answer 9

If I understood the problem correctly, your question is how to think to get loops right from the first try, not how to make sure your loop is right (for which the answer would be testing as explained in other answers).

What I consider a good approach is to write the first iteration without any loop. After you've done this, you should notice what it should be changed between iterations.

Is it a number, like a 0 or an 1? Then you most likely need a for, and bingo, you also have your starting i. Then think how many times you want to run the same thing, and you'll also have your end condition.

If you don't know EXACTLY how many times it will run, then you don't need a for, but a while or a do while.

Technically, any loop can be translated to any other loop, but the code is easier to read if you use the right loop, so here are some tips:

1. If you find yourself writing a if(){...;break;} inside a for, you need a while and you already have the condition

2. "While" is maybe the most used loop in any language, but it shouldn't imo. If you find yourself writing bool ok=True; while(check){ do something and hopefully change ok at some point}; then you don't need a while, but a do while, because it means that you have everything you need to run the first iteration.

Now a bit of context... When I first learned to program (Pascal), I didn't speak English. For me, "for" and "while", didn't make much sense, but the "repeat" (do while in C) keyword is almost the same in my mother tongue, so I would use it for everything. In my opinion, repeat (do while) is the most natural loop, because almost always you want something to be done and then you want it to be done again, and again, until a goal is reached. "For" is just a shortcut that gives you an iterator and weirdly places the condition at the beginning of the code, even though, almost always, you want something to be done until something happens. Also, while is just a shortcut for if(){do while()}. Shortcuts are nice for later, but the easiest way to get the loops right from the first try is to write them in the same way as your brain is thinking, which is "repeat(do) {something} until(while) (you have to stop)" and then use the appropriate shortcut if necessary.

Answer 10

I am going to give a more detailed example of how to use pre/post conditions and invariants to develop a correct loop. Together such assertions are called a specification or contract.

I am not suggesting that you try to do this for every loop. But I hope that you will find it useful to see the thought process involved.

In order to do so, I will translate your method into a tool called Microsoft Dafny, which is designed to prove the correctness of such specifications. It also checks termination of each loop. Please note that Dafny does not have a for loop so I have had to use a while loop instead.

Finally I will show how you can use such specifications to design an, arguably, slightly simpler version of your loop. This simpler loop version does infact have the loop condition j > 0 and the assignment array[j] = value - as was your initial intuition.

Dafny will prove for us that both of these loops are correct and do the same thing.

I will then make a general claim, based on my experience, about how to write correct backwards loop, that will perhaps help you if faced with this situation in the future.

Part One - Writing a specification for the method

The first challenge we are faced with is determining what the method is actually supposed to do. To this end I designed pre and post conditions which specify the behaviour of the method. To make the specification more exact I have enhanced the method to make it return the index where value was inserted.

method insert(arr:array<int>, rightIndex:int, value:int) returns (index:int)
  // the method will modify the array
  modifies arr
  // the array will not be null
  requires arr != null
  // the right index is within the bounds of the array
  // but not the last item
  requires 0 <= rightIndex < arr.Length - 1
  // value will be inserted into the array at index
  ensures arr[index] == value 
  // index is within the bounds of the array
  ensures 0 <= index <= rightIndex + 1
  // the array to the left of index is not modified
  ensures arr[..index] == old(arr[..index])
  // the array to the right of index, up to right index is
  // shifted to the right by one place
  ensures arr[index+1..rightIndex+2] == old(arr[index..rightIndex+1])
  // the array to the right of rightIndex+1 is not modified
  ensures arr[rightIndex+2..] == old(arr[rightIndex+2..])

This specification fully captures the behaviour of the method. My main observation about this specification is that it would be simplified if the procedure was passed the value rightIndex+1 rather than rightIndex. But since I cannot see where this method is called from I do not know what effect that change would have on the rest of the program.

Part Two - determining a loop invariant

Now we have a specification for the behaviour of the method, we have to add a specification of the loop behaviour that will convince Dafny that executing the loop will terminate and will result in the desired final state of array.

The following is your original loop, translated into Dafny syntax with loop invariants added. I have also changed it to return the index where value was inserted.

{
    // take a copy of the initial array, so we can refer to it later
    // ghost variables do not affect program execution, they are just
    // for specification
    ghost var initialArr := arr[..];


    var j := rightIndex;
    while(j >= 0 && arr[j] > value)
       // the loop always decreases j, so it will terminate
       decreases j
       // j remains within the loop index off-by-one
       invariant -1 <= j < arr.Length
       // the right side of the array is not modified
       invariant arr[rightIndex+2..] == initialArr[rightIndex+2..]
       // the part of the array looked at by the loop so far is
       // shifted by one place to the right
       invariant arr[j+2..rightIndex+2] == initialArr[j+1..rightIndex+1]
       // the part of the array not looked at yet is not modified
       invariant arr[..j+1] == initialArr[..j+1] 
    {
        arr[j + 1] := arr[j];
        j := j-1;
    }   
    arr[j + 1] := value;
    return j+1; // return the position of the insert
}

This verifies in Dafny. You can see it yourself by following this link. So your loop does correctly implement the method specification that I wrote in part one. You will need to decide if this method specification is really the behaviour that you wanted.

Note that Dafny is producing a proof of correctness here. This is a far stronger guarantee of correctness than can possibly be obtained by testing.

Part Three - a simpler loop

Now that we have a method specification that captures the behaviour of the loop. We can safely modify the implementation of the loop while still retaining confidence that we have not changed the loop behaviour.

I have modified the loop so that it matches your original intuitions about the loop condition and final value of j. I would argue that this loop is simpler than the loop you described in your question. It is more often able to use j rather than j+1.

1. Start j at rightIndex+1

2. Change the loop condition to j > 0 && arr[j-1] > value

3. Change the assignment to arr[j] := value

4. Decrement the loop counter at the end of the loop rather than the begining

Here is the code. Note that the loop invariants are also somewhat easier to write now:

method insert2(arr:array<int>, rightIndex:int, value:int) returns (index:int)
  modifies arr
  requires arr != null
  requires 0 <= rightIndex < arr.Length - 1
  ensures 0 <= index <= rightIndex + 1
  ensures arr[..index] == old(arr[..index])
  ensures arr[index] == value 
  ensures arr[index+1..rightIndex+2] == old(arr[index..rightIndex+1])
  ensures arr[rightIndex+2..] == old(arr[rightIndex+2..])
{
    ghost var initialArr := arr[..];
    var j := rightIndex+1;
    while(j > 0 && arr[j-1] > value)
       decreases j
       invariant 0 <= j <= arr.Length
       invariant arr[rightIndex+2..] == initialArr[rightIndex+2..]
       invariant arr[j+1..rightIndex+2] == initialArr[j..rightIndex+1]
       invariant arr[..j] == initialArr[..j] 
    {
        j := j-1;
        arr[j + 1] := arr[j];
    }   
    arr[j] := value;
    return j;
}

Part Four - advice about backward looping

After having written and proved correct many loops over quite a few years, I have the following general advice about looping backwards.

It is almost always easier to think about and write a backward (decrementing) loop if the decrement is performed at the beginning of the loop rather than the end.

Unfortunately the for loop construct in many languages makes this difficult.

I suspect (but cannot prove) that this complexity is what caused the difference in your intuition about what the loop should be and what it actually needed to be. You are used to thinking about forward (incrementing) loops. When you want to write a backward (decrementing) loop you try to create the loop by trying to reverse the order that things happen in a forward (incrementing) loop. But because of the way the for construct works you neglected to reverse the order of the assignment and loop variable update - which is needed for a true reversal of the order of operations between a backward and forward loop.

Part Five - bonus

Just for completeness, here is the code you get if you pass rightIndex+1 to the method rather than rightIndex. This changes eliminates all the +2 offsets that are otherwise required to think about the correctness of the loop.

method insert3(arr:array<int>, rightIndex:int, value:int) returns (index:int)
  modifies arr
  requires arr != null
  requires 1 <= rightIndex < arr.Length 
  ensures 0 <= index <= rightIndex
  ensures arr[..index] == old(arr[..index])
  ensures arr[index] == value 
  ensures arr[index+1..rightIndex+1] == old(arr[index..rightIndex])
  ensures arr[rightIndex+1..] == old(arr[rightIndex+1..])
{
    ghost var initialArr := arr[..];
    var j := rightIndex;
    while(j > 0 && arr[j-1] > value)
       decreases j
       invariant 0 <= j <= arr.Length
       invariant arr[rightIndex+1..] == initialArr[rightIndex+1..]
       invariant arr[j+1..rightIndex+1] == initialArr[j..rightIndex]
       invariant arr[..j] == initialArr[..j] 
    {
        j := j-1;
        arr[j + 1] := arr[j];
    }   
    arr[j] := value;
    return j;
}

Answer 11

Getting this right easily and fluently is a matter of experience. Even though the language doesn't let you express it directly, or you're using a more complex case than the simple built-in thing can handle, what you think is a higher level like "visit each element once in revere order" and the more experienced coder translates that into the right details instantly because he's done it so many times.

Even then, in more complex cases it's easy to get wrong, because the thing you're writing is typically not the canned common thing. With more modern languages and libraries, you don't write the easy thing because there is a canned construct or call for that. In C++ the modern mantra is "use algorithms rather than writing code".

So, the way to make sure it's right, for this kind of thing in particular, is to look at the boundary conditions. Trace through the code in your head for the few cases on the edges of where things change. If the index == array-max, what happens? What about max-1? If the code makes a wrong turn it will be at one of these boundaries. Some loops need to worry about the first or last element as well as the looping construct getting the bounds right; e.g. if you refer to a[I] and a[I-1] what happens when I is the minimal value?

Also, look at cases where the number of (correct) iterations is extreme: if the bounds are meeting and you will have 0 iterations, will that just work without a special case? And what about just 1 iteration, where the lowest bound is also the highest bound at the same time?

Examining the edge cases (both sides of each edge) is what you should do when writing the loop, and what you should do in code reviews.

Answer 12

I'll try to stay clear of the topics mentioned galore already.

What are tools/mental models to avoid such mistakes?

Tools

For me, the biggest tool to write better for and while loops is not to write any for or while loops at all.

Most modern languages try to target this problem in some fashion or other. For example, Java, while having Iterator right from the start, which used to be a bit clunky to use, introduced short-cut syntax to use them easier in a latler release. C# has them as well, etc.

My currently favoured language, Ruby, has taken on the functional approach (.each, .map etc.) full-front. This is very powerful. I just did a quick count in some Ruby code-base I'm working on: in about 10.000 lines of code, there are zero for and about 5 while.

If I were forced to pick a new language, looking for functional/data based loops like that would be very high on the priority list.

Mental models

Keep in mind that while is the barest minimum of abstraction you can get, just one step above goto. In my opinion, for makes it even worse instead of better since it chunks all three parts of the loop tightly together.

So, if I am in an evironment where for is used, then I make damn sure that all 3 parts are dead simple and always the same. This means I will write

limit = ...;
for (idx = 0; idx < limit; idx++) { 

But nothing very more complex. Maybe, maybe I'll have a countdown sometimes, but I will do my best to avoid it.

If using while, I stay clear of convoluted inner shenannigans involving the loop condition. The test inside the while(...) will be as simple as possible, and I will avoid break as best I can. Also the loop will be short (counting lines of code) and any larger amounts of code will be factored out.

Especially if the actual while condition is complex, I will use a "condition-variable" which isvery easy to spot, and not place the condition into the while statement itself:

repeat = true;
while (repeat) {
   repeat = false; 
   ...
   if (complex stuff...) {
      repeat = true;
      ... other complex stuff ...
   }
}

(Or something like that, in the correct measure, of course.)

This gives you a very easy mental model which is "this variable is running from 0 to 10 monotonously" or "this loop runs until that variable is false/true". Most brains seem to be able to handle this level of abstraction just fine.

Hope that helps.

Answer 13

Reverse loops, in particular, can be difficult to reason about because many of our programming languages are biased toward forward iteration, both in the common for-loop syntax and by the use of zero-based half-open intervals. I'm not saying that it's wrong that the languages to made those choices; I'm just saying that those choices complicate thinking about reverse loops.

In general, remember that a for-loop is just syntactic sugar built around a while loop:

// pseudo-code!
for (init; cond; step) { body; }

is equivalent to:

// pseudo-code!
init;
while (cond) {
  body;
  step;
}

(possibly with an extra layer of scope to keep variables declared in the init step local to the loop).

This is fine for many kinds of loops, but having the step come last is awkward when you're walking backwards. When working backwards, I find it's easier to start the loop index with the value after the one I want and to move the step portion to the top of the loop, like this:

auto i = v.size();  // init
while (i > 0) {  // simpler condition because i is one after
    --i;  // step before the body
    body;  // in body, i means what you'd expect
}

or, as a for loop:

for (i = v.size(); i > 0; ) {
    --i;  // step
    body;
}

This can seem unnerving, since the step expression is in the body rather than the header. That's an unfortunate side effect of the inherent forward-bias in for loop syntax. Because of this, some will argue that you instead do this:

for (i = v.size() - 1; i >= 0; --i) {
    body;
}

But that's a disaster if your index variable is an unsigned type (as it might be in C or C++).

With this in mind, let's write your insertion function.

1. Since we'll be working backward, we'll let the loop index be the entry after the "current" array slot. I would design the function to take the size of the integer rather than an index to the last element because half-open ranges are the natural way to represent ranges in most programming languages and because it gives us a way to represent an empty array without resorting to a magic value like -1.

   function insert(array, size, value) {
     var j = size;
   

2. While the new value is smaller than the previous element, keep shifting. Of course, the previous element can be checked only if there is a previous element, so we first have to check that we're not at the very beginning:

     while (j != 0 && value < array[j - 1]) {
       --j;  // now j become current
       array[j + 1] = array[j];
     }
   

3. This leaves j right where we want the new value.

     array[j] = value; 
   };
   

Programming Pearls by Jon Bentley gives a very clear explanation of insertion sort (and other algorithms), which can help build your mental models for these kinds of problems.

Answer 14

Are you simply confused about what a for loop actually does and the mechanics of how it works?

for(initialization; condition; increment*)
{
    body
}

1. First, the initialization is executed
2. Then the condition is checked
3. If the condition is true, the body is run once. If not goto #6
4. The increment code is executed
5. Goto #2
6. End of loop

It might be useful for you to rewrite this code using a different construct. Here's the same using a while loop:

initialization
while(condition)
{
    body
    increment
}

Here are some other suggestions:

• Can you use another language construct like a foreach loop? This takes care of the condition and increment step for you.
• Can you use a Map or Filter function? Some languages have functions with these names that internally loop through a collection for you. You just supply the collection and the body.
• You should really spend more time familiarizing yourself with for loops. You'll use them all the time. I suggest that you step through a for loop in a debugger to see how it executes.

* Note that while I use the term "increment", it's just some code that's after the body and before the condition check. It can be a decrement or nothing at all.

Answer 15

Attempt of additional insight

For non-trivial algorithms with loops, you could try the following method:

1. Create a fixed array with 4 positions, and put some values in, to simulate the problem;
2. Write your algorithm to solve the given problem, without any loop and with hard-coded indexings;
3. After that, substitute hard-coded indexings in your code with some variable i or j, and increment/decrement these variables as necessary (but still without any loop);
4. Rewrite your code, and put the repetitive blocks inside a loop, fulfilling the pre and post conditions;
5. [optional] rewrite your loop to be in the form you want (for/while/do while);
6. The most important is to write your algorithm correctly; after that, you refactor and optmize your code/loops if necessary (but this might make the code non-trivial anymore for a reader)

Your problem

//TODO: Insert the given value in proper position in the sorted subarray
function insert(array, rightIndex, value) { ... };

Write the body of the loop manually multiple times

Let's use a fixed array with 4 positions and try to write the algorithm manually, without loops:

           //0 1 2 3
var array = [2,5,9,1]; //array sorted from index 0 to 2
var leftIndex = 0;
var rightIndex = 2;
var value = array[3]; //placing the last value within the array in the proper position

//starting here as 2 == rightIndex

if (array[2] > value) {
    array[3] = array[2];
} else {
    array[3] = value;
    return; //found proper position, no need to proceed;
}

if (array[1] > value) {
    array[2] = array[1];
} else {
    array[2] = value;
    return; //found proper position, no need to proceed;
}

if (array[0] > value) {
    array[1] = array[0];
} else {
    array[1] = value;
    return; //found proper position, no need to proceed;
}

array[0] = value; //achieved beginning of the array

//stopping here because there 0 == leftIndex

Rewrite, removing hard-coded values

//consider going from 2 to 0, going from "rightIndex" to "leftIndex"

var i = rightIndex //starting here as 2 == rightIndex

if (array[i] > value) {
    array[i+1] = array[i];
} else {
    array[i+1] = value;
    return; //found proper position, no need to proceed;
}

i--;
if (i < leftIndex) {
    array[i+1] = value; //achieved beginning of the array
    return;
}

if (array[i] > value) {
    array[i+1] = array[i];
} else {
    array[i+1] = value;
    return; //found proper position, no need to proceed;
}

i--;
if (i < leftIndex) {
    array[i+1] = value; //achieved beginning of the array
    return;
}

if (array[i] > value) {
    array[i+1] = array[i];
} else {
    array[i+1] = value;
    return; //found proper position, no need to proceed;
}

i--;
if (i < leftIndex) {
    array[i+1] = value; //achieved beginning of the array
    return;
}

//stopping here because there 0 == leftIndex

Translate to a loop

With while:

var i = rightIndex; //starting in rightIndex

while (true) {
    if (array[i] > value) { //refactor: this can go in the while clause
        array[i+1] = array[i];
    } else {
        array[i+1] = value;
        break; //found proper position, no need to proceed;
    }

    i--;
    if (i < leftIndex) { //refactor: this can go (inverted) in the while clause
        array[i+1] = value; //achieved beginning of the array
        break;
    }
}

Refactor/rewrite/optimize the loop the way you want:

With while:

var i = rightIndex; //starting in rightIndex

while ((array[i] > value) && (i >= leftIndex)) {
    array[i+1] = array[i];
    i--;
}

array[i+1] = value; //found proper position, or achieved beginning of the array

with for:

for (var i = rightIndex; (array[i] > value) && (i >= leftIndex); i--) {
    array[i+1] = array[i];
}

array[i+1] = value; //found proper position, or achieved beginning of the array

PS: code assumes input is valid, and that array does not contain repetitions;

Answer 16

This is why I would avoid writing loops that operate on raw indices, in favor of more abstracted operations, whenever possible.

In this case, I would do something like this (in pseudo code):

array = array[:(rightIndex - 1)] + value + array[rightIndex:]

Answer 17

In your example, the body of the loop is quite obvious. And it is quite obvious that some element has to be changed at the very end. So you write the code, but without the start of the loop, the end condition, and the final assignment.

Then you go away from the code and find out which is the first move that needs to be performed. You change the start of the loop so that the first move is correct. You go away from the code again and find out which is the last move that needs to be performed. You change the end condition so that the last move will be correct. And finally, you go away from your code and figure out what the final assignment must be, and fix the code accordingly.