Loops – Provability of While Loop vs For Loop

loops

I have this teacher, he's quite smart (sometimes, haha) he said good programmers try to use while loops instead of for loops. the reason he gave for this is because while loops can be proven, as in, one can completely explain what happens in a while loop whereas you can't do that for a for loop. he also said something about NASA programmers only using while loops and not allowed to do for loops because of this.

I have quite a hard time understand this, for both loops one can explain how they work in detail right? for both you would always know what is going to happen?

can someone explain to me why while loops can be proven (And because of it, might be better than for loops, in some cases at least).

EDIT:
maybe he was reffering to:
2: All loops must have a fixed upper bound. It must be trivially possible for a checking tool to statically prove that a preset upper bound on the number of iterations of a loop cannot be exceeded. If the loop-bound cannot be proven statically, the rule is considered violated.

Though this still doesn't say anything about the difference between while and for loops.

Best Answer

In a nutshell: What your teacher probably meant is that the semantics of while is pretty much the same in most languages, while the semantics of for may change considerably (see discussion below). Hence, abstract language independent proof are more reliable with a while, but one should be careful that a proof with a for loop may not match the semantics of the for loop in many languages.

Your question is not precise enough (though that may not be your fault).

The point is that, afaik, there is no official, ISO supported standard, or otherwise officially accepted reference definition of for and while loops. The definition depends on the programming language.

Hence you cannot make any general statement regarding their equivalence before you have defined precisely what each can do. I adress that more precisely, since it is one of the main argument used in other answers (and the discussion will be useful in what follows).

On intertranslatability of `for` and `while` loops

Summary: it depends on the programming language, but is always possible a long as you can have one infinite loop and a way to get out of it.

But you can make such a statement for a specific programming language, and the answer will depend on the features fo the language.

That also means that there is no general proof, but only one for each programming language.

One thing that is generally true is that a while loop can generally mimic a for loop, because the while loop can do the exit condition testing of the for loop, doing the initialisation of the control variable with an assignment before entering the loop, and doing the incrementation at the end of the loop body, so that

for i from 1 by 2 to 10 do { xxx }

becomes

i=1
while i≤11 do { xxx; i←i+2 }

This more or less works for most languages, but it is not as obvious as it seem, and there may be many "details" to worry about.

For example, in many languages, the for loop evaluates it 3 arguments (initial value, increment, and final value) as strict arguments, evaluated once before entering the loop, while others will take then as thunk arguments to be reevaluated at each turn, or possibly as lazy argument to be evaluated only when first needed.

Another point may be that the increment variable may be local to the for loop, or have to be a local variable of the function where the loop appears.

Depending on such issues, the translation of a for to a while may vary widely, though it is usually possible to achieve it.

The same holds for the converse, thranslating a while into a for loop.

Th first problem is that a while loop will always reevaluate the exit condition at each turn. But some for loops do not provide for a condition that is reevaluated at each turn, other than comparison of the control variable with some fixed value computed on loop entry. Then the translation is not possible unless there is some other mean to jump out of the loop on some arbitrary conditions.

That is achievable with various devices, usually starting with a conditional statement testing the condition, followed by an a jump out implemented, as available, by a loop exit statement, a return statement (after encapsulating the loop in a function), a goto statement or an exception raising.

In other words, it is again very dependent on languages, and possibly on subtle features of languages.

This say, as answered by @milleniumbug, the intertranslation is easy in the language C, because a for lopp is essentially a while loop plus some extra for an incremented control variable.

But this does not necessarily apply to other languages, and most likely not in the same way.

This being said, programming languages are usually supposed to have Turing power with only one of these loops, since all you need for it is one infinite loop. So, as long as you have some way of looping for ever, and possibly deciding to stop, you are pretty sure you can mimic any other construct ... but not necessarily easily.

Regarding proofs

Summary: There is no reason known to me to assert that proofs should be significantly harder with one or the other (unless some weird feature of the language).

There is probably a misunderstanding, or your teacher had his mind on something else.

Formals semantics can be defined for the various kinds of loops defined in programming languages, and then used for proving properties.

It may be, again depending on the language, that conducting formal proofs regarding programs may be more complex in some cases. But that depends on the language.

I cannot imagine a reason why proofs should be significantly harder with one construct more than with the other. The for loop may be more complex since it can offer, as in C, all that is done with a while plus other things. But if you did it with a while, you would have to add the extras in some other form.

I could use the formal general argument of intertranslatability, as long as there is the possibility for a single infinite loop. I will however refrain from doing that, as the constructions involved are nothing you want to deal with in a proof, and it would clearly be an unfair statement, at least in practice.

Following the above discussion, however, we have seen that the difficulties for intertranslatability come from the great variability of the for loop from language to language. Hence the following conclusion which is probably the right answer:

One possibility to understand your teacher's statement is that the semantics of the while loop is pretty much the same in all programming languages, while the syntax and semantics of the for loop can vary significantly from language to language. Hence, it is possible to make general "abstract" proofs with while loops that have language independent semantics to a good extent, while this is not possible for the for loop that has syntax and semantics changing too much from language to language. But this does not apply within a given language, when the semantics of both are precisely defined.

My best suggestion is that you should ask your teacher what he precisely meant, and whether he can give you an example. Misphrasing or misunderstanding is a common event.

Related Solutions

Algorithms – Complexity in Nested Loops

You seem to think that the complexity of an algorithm is linked to the number of nested loops. It is not the case. The following piece of code is O(1):

for i in [1.. 10^15]:
    for j in [1.. 10^15]:
        for k in [1.. 10^15]:
            dosomethingO1()

Complexity is related to the rate of growth of the number of operations. Unrolling your loop does not change that. So:

foreach(element in myArray) {
    doSomeAction(element);
}

Has 0(1) if the number of elements in myArray is bounded. The complexity will be decided by the number of iterations in the while loop.

About your grid example: if n is the number of cells and your grid is represented as a nested array, looping over those arrays still yields O(n) complexity.

SQL Algorithms – Is There a Purely SQL Alternative to Looping?

Depending on your version of SQL Server, windowing functions will do what you want. 2008 has limited support but 2012 adds nearly all of the standard. The over clause is used for things exactly like this, it is also available in the express versions as well.

http://technet.microsoft.com/en-us/library/ms189461.aspx

Windowing functions are used to perform high-level aggregation, ranking and statistical analysis. They are often used to split and show similarities in a data set.

The over clause can partition a column and provide a running sum like you describe in a T-SQL Statement.

SELECT [id], [vendor_id], [item], [brand], [inventory_version], SUM([quantity])
    OVER (PARTITION BY [vendor_id], [item]
        ORDER BY [vendor_id], [item], [inventory_version]) AS qty_Totals
FROM inventory_snapshots
ORDER BY [vendor_id], [item], [inventory_version]

Code is untested but should work. What it does is take the recordset, partitions it by the vendor_id and item. This effectively resets the sumation to 0 when that combination changes. We make sure to order the results in a logical manner to show the running totals easily. This will show the progression of item versions per manufacturer starting at the lowest and going straight through to the last.

Hopefully this clears things up a bit.