[pjmlp]

> For example, they always terminate.

How do you terminate?

   for(;;) {
   }

[meggar]

break;

[pjmlp]

Not all programming languages have break; C syntax was just an example.

Also break is no different from using return (to keep C syntax as example) when recursing.

If you guard break with if then you also need to prove if the "if" condition does indeed provide a dataflow path to break.

[AnimalMuppet]

> If you guard break with if then you also need to prove if the "if" condition does indeed provide a dataflow path to break.

In all cases, for all possible inputs.

On the other hand, if that's what your for loop looks like, you probably have the same problem of proving that your recursion terminates (in all cases, for all possible inputs).

[pjmlp]

Of course, I was just arguing against the OP that all loops terminate.