18
$\begingroup$

I'm trying to teach a friend to code in Python. I've noticed that whenever they write a while loop with an integer increment, such as the one shown below:

i = 0
while i < 10:
    do this
    i += 1

...they always seem to leave out the i += 1 at the end, which causes an infinite loop.

How can a linter or something similar check for this error and notify the user?

$\endgroup$
0

7 Answers 7

39
$\begingroup$

Low-hanging fruit

Of course, the halting problem is undecidable. However, linters don't have to be perfectly logical, because they emit warnings that aren't even from the code itself (i.e. they can be completely bypassed by not using the IDE).

A huge fraction of errors of this sort will involve the situation where none of the identifiers in the while expression are used at all in the loop body, and there is also no explicit break, return or other deliberate exit. Technically, such a loop could still terminate (say, if the expression involves a call to a function that has side effects, or an exception is raised), but in the vast majority of cases, code shaped like this will be problematic. So a rule like this is Good Enough for a linter.

$\endgroup$
8
  • 3
    $\begingroup$ Don't forget the break statements (if your language has them). $\endgroup$
    – Vilx-
    Jul 22, 2023 at 14:00
  • $\begingroup$ Linters do have to be perfectly logical, because they are deterministic algorithms running on deterministic computers. Whether they ever produce false negatives is another matter. $\endgroup$ Jul 22, 2023 at 14:10
  • 4
    $\begingroup$ Yes, that's the important thing: undecidable. However it could probably be done rigorously if the behaviour were detectable at compilation time, i.e. no functions with side-effects invoked etc., no parallel processing, no interrupt handlers... ... all in all, it might be better simply to teach the student that it's something to watch out for. $\endgroup$ Jul 22, 2023 at 14:41
  • $\begingroup$ @Vilx- edited accordingly. $\endgroup$ Jul 22, 2023 at 18:18
  • 5
    $\begingroup$ @user3840170 I don't mean "could perform illogically"; I mean "are not required to implement logic that perfectly addresses the problem". $\endgroup$ Jul 22, 2023 at 18:19
27
$\begingroup$

It is often possible to determine that a loop terminates, or doesn't terminate, through static analysis. While it isn't always possible to determine whether a loop terminates or not, it's a category error to think that this means it's never possible — in fact, it is frequently possible to detect non-terminating loops automatically.

Verifying languages like Whiley and Dafny can enforce that loops terminate by checking loop invariants, preconditions, and termination conditions with theorem provers. Sometimes the programmer needs to provide additional annotations to assist the prover when it rejects a program because it couldn't be certain of termination.

In the case of a simple Dafny loop

var i := 0;
while i < n
{
  // ... do something ...
}

the compiler will correctly reject this program as non-terminating, while if i := i + 1 were inside the body then the termination checker would verify the program. It infers a loop variant decreases n - i from the loop's test condition, and it can easily see that this expression will not decrease because neither i nor n changes within the loop. The termination checker will often just work without further effort from the programmer, even for moderately complex loops.

In still-more-complex loops, the programmer will need to specify loop invariants, pre- and post-conditions, or manual decreases conditions. The verifier will ensure that the program is consistent with these annotations, and that they guarantee the necessary properties. Otherwise, the compiler will reject the program and report to the user with a diagnostic message saying why.

$\endgroup$
1
  • 2
    $\begingroup$ My feeling is that this is much more confusing for a beginner than simply allowing them to run the program and see it loop forever. In particular, if they have to annotate their loops to prove they terminate, or if the error is anything more complex than "loop never ends", they'll never get into the language at all. I think that a beginner has to make a mistake like this, see the immediate consequences, and then eventually they will appreciate having tools to avoid the mistake, but only after the mistake frustrates them. $\endgroup$
    – user253751
    Jul 24, 2023 at 10:35
20
$\begingroup$

Having "for each" loops instead of, or in addition to, "while" loops

In Python you'd typically loop like:

for i in range(10):
    do this

You don't need to remember to increment i, since the iterator will run over all values.

This also makes it easy to loop over arrays or or other data structures since you don't need to know the length.

Disadvantage is you can't change the value of i inside the loop depending on conditions, at least not without writing your own generator.

Having a built-in "update slot" in your loop so you know if something is missing

In C-style languages, you have the 3 part for loop like this:

for(int i=0; i<10; i++) {

}

While you can of course omit the i++ if you want:

for (int i=0; i<10;) {}

However, the slot is still there, will look weird and empty, and act as a sort of "are you sure" spot. If you do want to skip the increment you are making it more explicit.

Deciding whether a loop will terminate in a linter is undecidable

That's basically the halting problem. I'd focus instead on designing the language to encourage less error-prone types of loops when possible.

Other methods mentioned in other answers do work, but they require a highly restricted language to be able to effectively rule out side effects and overloads effecting the loop condition.

Even if you do manage to eliminate all possible factors that could cause termination, you still don't know if the loop being infinite is intentional or a mistake. I call this "the meta halting problem": "Given a oracle for the halting problem, it is still undecidable if the developer intended for this Turing machine to halt."

$\endgroup$
5
  • 2
    $\begingroup$ I recently had to write code with one of the three "slots" in a C-style for loop was empty. Yes, it looks weird, and that's the point. $\endgroup$
    – Bbrk24
    Jul 22, 2023 at 18:32
  • 2
    $\begingroup$ Minor correction: as pointed out by Michael Homer's answer, a better way to put it is "Deciding whether every loop will terminate in a linter is undecidable". The majority of loops can be relatively easily determined whether they terminate or not, it's just that there always exists at least one way to code a loop where it can't be determined. $\endgroup$
    – Idran
    Jul 24, 2023 at 13:54
  • 1
    $\begingroup$ @JustinHilyard True, in a way, but the methods mentioned in the other answers are really error prone to implement right, and you can easily create a situation causing unnecessary errors or warnings. $\endgroup$
    – mousetail
    Jul 24, 2023 at 14:01
  • 1
    $\begingroup$ +1 for using better tools first. for loops should be the goto. while loops should only be used when the condition/iteration is tricky. Not only does this guideline means you'll avoid iteration issues most of the time (by using for), it also means that any while loop should get extra scrutiny with regard to its iteration, and therefore any mistake there is more likely to be caught. $\endgroup$ Jul 25, 2023 at 7:06
  • $\begingroup$ One thing to note about for-each loops is that if iterators can be user-defined ─ which they can in most languages that have for-each loops ─ then it's no longer guaranteed that for-each loops terminate, because the user can define an infinite iterator. As an aside, "the goto" is a funny way of describing which control-flow statement should be preferred :D $\endgroup$
    – kaya3
    Aug 7, 2023 at 14:53
15
$\begingroup$

Some languages allow only loops that can be proved to terminate.

One example of this is eBPF, which includes a bytecode verification step before a program is allowed to run:

... the program is only accepted if the verifier can ensure that the loop contains an exit condition which is guaranteed to become true.

The verifier avoids the Halting Problem by rejecting programs that are too complex for verification within a reasonable budget:

Program must have a finite complexity. The verifier will evaluate all possible execution paths and must be capable of completing the analysis within the limits of the configured upper complexity limit.

$\endgroup$
2
  • 6
    $\begingroup$ Another such example - total functional programming, where recursion is always guaranteed to terminate. $\endgroup$
    – SK-logic
    Jul 22, 2023 at 10:51
  • $\begingroup$ A loop that is proved to terminate after 2^64 is practically infinite. $\endgroup$
    – gnasher729
    Jul 25, 2023 at 15:30
9
$\begingroup$

Transforming into Pure, Tail-Recursive Functions Could Help

Or equivalently, static single assignments and blocks, but tail-recursion is nicer for humans to write.

The advantage here is that it greatly simplifies the analysis. The only way the state can change is to make a tail-call and change all of it at once. The only quantities that can change are the parameters of the function, which are normally listed for you. (This begins to get complicated when you do things like update an array, or make mutually-recursive tail calls, but it’ll do for this special case.

It will be much more convenient to write our loops if we allow certain provably-safe extensions to the subset we can analyze, such as tail-recursion modulo cons.

Another important reason to work on this representation is, most major compilers transform the source code into an intermediate representation in either CPS or SSA form, so an analyzer might be able to work on the IR.

Annotating to Prove Termination

A simple example of some hypothetical syntax:

{- terminating{i > 0} -}
factorial::(Unsigned -> Unsigned)
factorial 0 = 1
factorial i = i * factorial (i-1)

If we’d written this as a while loop in an imperative language, i>0 would have been the loop condition, so this syntax should be intuitive.

Side note: in actually-existing functional languages, you’re more likely to see this expressed as:

factorial::(Unsigned -> Unsigned)
factorial n = go 1 n where
    {- terminating{i > 0} -}
    go accumulator 0 = accumulator
    go accumulator i = go (accumulator*i) (i-1)

But in fact the same optimization that allows tail-recursion modulo cons applies to any semigroup operation on a variable. So I’m just going to assume that our language is smart enough to compile the tail-recursion-modulo-semigroup version efficiently, even though I don’t think compilers in 2023 actually now do this in general and not just for a few special cases. (I would love to find out that I’m wrong.)

In this context, the annotation tells an analyzer what to check: that every branch of the function either terminates the loop, or calls the function with the new value of i both greater than or equal to zero, and decreasing. If these conditions are satisfied, the loop provably terminates. But if the reason the programmer gave us for believing that the loop terminates was that i decreases to 0, and we can’t convince ourselves that it does, that’s concerning.

Extending the Syntax

For symmetry, there should of course be a < condition:

sum container  = go 0 where
    n = length container
    {- terminating{i < n} -}
    go i | i == n    = 0
         | otherwise = container!i + sum (i+1)

{This punts on one of the tricky little problems, proving that length container is finite, but since I moved that outside the loop, it’s no longer the loop-analyzer’s problem.)

But what if we want an extension of the factorial over all the integers?

{- terminating{|i| > 0} -}
factorialEx::(Integer->Integer)
factorialEx 0             = 1
factorialEx i | i < 0     = -1 * factorialEx(-i - 1)
              | otherwise = i * factorialEx(i - 1)

A Canonical Form

Counting down the absolute value of some quantity toward zero is such a common terminating condition, I’ll delare it the default in this syntax:

{- terminating{i} -}

We can easily see that the other two examples so far could also be expressed this way. Clearly, FactorialEz also has the terminating condition {i}.

We can turn a comparison into a difference very easily:

sum container  = go 0 where
    n = length container
    {- terminating{n - i} -}
    go i | i == length container = 0
         | otherwise             = container!i + sum (i+1)

Expressions as Terminating Conditions

Sometimes, the well-founded termination condition doesn’t explicitly appear in the code at all, though. Take for example this merge of ordered lists:

{- terminating{length first + length second} -}
merge first@[]     second@[]                 = []
merge first        second@[]                 = first
merge first@[]     second                    = second
merge first@(x:xs) second@(y:ys) | y < x     = y:(merge first ys)
                                 | otherwise = x:(merge xs second)

We can only verify this for all branches if we know that the length of a non-empty list is always larger than the length of its tail, so let’s extend this syntax in an ad-hoc way to be able to tell the compiler that:

{- terminating{ length [] = 0, length (x:xs) = length xs + 1 ;
                length first + length second } -}

In practice, such a commonly-used fact should be defined in the standard library, so the compiler remembers it without being told.

Algorithmically Guessing the Condition

Will this work for everything? No, of course not. Since you’re still reading this far, you’ve seen Alan Turing’s proof that nothing can. But, in practice, a lot of loops are simple enough to check with a couple of heuristics.

There are usually a small number of variables, two or three, that appear in a terminating condition, and a slightly-larger number of local variables with the right type to make up an arithmetic expression that evaluates to a condition in canonical form, which we know must include at least one of the parameters that gets changed in every call on every branch—if any branch calls the same pure function with the same arguments, that would be an infinite loop. There are only eight possible arrangements of a, b, and c of the form (a + b + c), (a + b - c), (a - b + c), etc. There are only three of the form a * (b + c) and another three of the form a + bc. There are only six of the form a * (b - c) and six of the form a + (b/c). Check these first.

As this number gets higher, we of course get a combinatorial explosion. But a human code reviewer would tell a programmer not to write loops with a huge amount of internal state to keep track of, too. and restricting ourselves to functional programming makes it much easier to see what the possible variables are.

Future Directions

A few of the most useful ways this might be extended:

  • Inferring a loop condition that relies on a combination of facts, rather than a single, explicitly-spelled-out fact.
  • Mutual recursion, with conditions that need to span two different functions.
  • Constraints on the data
  • An annotation meaning, “This branch doesn’t bring the loop closer to termination, but as you can verify, the recursive call it makes will take a branch that does.”
  • Disjunctions in the list of givens. For example, either x < y, or x < y, or x == y.
  • Implications. For example, if x > y, y < x.

Update: Arbitrary State Variables as Conditions

One idea that came to me last night and I’d like to know if someone has implemented is that many modern languages support sum types (such as Haskell data or Rust enum), and allow the user to define an ordering, partial or total, over them. If this actually is a true partial ordering, this would allow the compiler to prove the correctness of a loop as general as

{- terminating{terminalState} -}
loop terminalState = extractResult state
loop state         = loop (update state)

where this checks that, on every branch that makes a tail-recursive call that updates state to state', either state < state'terminalState' or state>state'terminalState`.

This wouldn’t work on loops with more than one possible terminal state that a loop might bounce between. In that case, you’d also need to show that the next branch also moves the state even closer to the same terminal state.

A programmer who had this might even write an ordering function that won’t generate executable code, just so the compiler can see it and automatically deduce that the loop terminates. (It would probably help convince a human that the loop terminates, too.)

So, Whose Wheel Did I Just Re-Invent?

I’d be surprised if someone hasn’t worked this out already in much more detail, and published it. I’d appreciate the citations!

$\endgroup$
2
  • $\begingroup$ I believe this is similar to imperative languages that prove loop termination. However, your idea to mark a countdown as a function argument is interesting because it changes the proof requirement. Now you have to prove that in any recursive call, the recursive parameter i is smaller than the current parameter i and greater than zero, and this is a trivial proof in many cases (e.g. in factorialEx). However, having to specify that i counts down is still uselessly obscure to the beginner. $\endgroup$
    – user253751
    Jul 24, 2023 at 10:40
  • $\begingroup$ @user253751 Thanks. The basic idea is that it might be trivial enough for an algorithm to deduce it on its own. And in the cases where it can’t, and asks the programmer to write a proof, the proof language can be as close to the HLL as possible: the proof is, writing out the function that counts down. $\endgroup$
    – Davislor
    Jul 24, 2023 at 14:09
5
$\begingroup$

While it is not possible to solve this problem in general (see the halting problem) it is certainly possible to solve it in some very common cases.

For example, in C# if you enter this:

var i = 0;
while (i < 10) {
    Console.WriteLine(i);
}

The editor will put a wiggly line under the while condition and warn that "this condition is always true." FWIW, I'd prefer it considered it an actual error, but that is beside the point. In the specific case you mention it is certainly solvable.

The data flow analysis of the compiler can determine which variables can be changed and in what part of the code. Here is is relatively simple since the variable is local, and so has visibility only in the block, and the parameter passed to Console.Writeline is pass by value. It is certainly possible to do it at a larger scale by tracing what functions can change what variables. For example if this was a property of a class, if private you can readily determine which methods in the class can change that property, since they are the only ones that have access to it.

In languages like C++ this ability is enhanced by the use of const correctness, where the programmer can explicitly specify to the compiler (and the compiler can enforce) these types of rules, enhancing the ability of the dfa to detect this sort of thing.

So it can be done, and it often is done, for many of the most common cases. It can't be done for all cases, and it is harder in lower level languages like C++ where references to variables and aliases can rather easily be hidden, especially if the programmer isn't careful about their const correctness. In these cases the compiler will still produce correct code, just that it'll be more conservative, and more of the "common cases" I mentioned will be considered indeterminable.

I'm not a Python guy, but for sure Python COULD do this too. If it doesn't I'd consider that a shortcoming in the compiler or interpreter you are using.

$\endgroup$
3
  • $\begingroup$ I would not recommend making this an actual error because there is more stuff to understand before you can understand the error. The beginner may not understand why the error is there, without reading a bunch of theory - until he actually runs the program and it loops forever, and then he will instantly understand it. The epiphany can't happen if you stop him from running the program. $\endgroup$
    – user253751
    Jul 24, 2023 at 10:41
  • $\begingroup$ Aside from that, it's useful to be able to write programs that don't offer an explicit exit. $\endgroup$ Jul 24, 2023 at 16:55
  • $\begingroup$ @KarlKnechtel that's an excellent point. There is the classic for(;;) C idiom. But for sure I'd upgrade it to a warning at least. $\endgroup$
    – Fraser Orr
    Jul 25, 2023 at 4:40
2
$\begingroup$

Simplest check that some languages are already doing is to see if any variables involved in the loop condition check are modified, or otherwise if any break or return statement exists in the loop.

While this is not always (reading from the default input stream would change the loop condition without modifying any visible variables), this would catch majority of errors.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .