I'm pretty sure that running is false when the program reaches the end of the while loop, whether it is assigned in the loop or not. I only added the "don't assign to running" to make the example match your pattern.
Well, if you don't assign to it in the loop, and it is known to terminate, then "running" is provably false before the loop for sure?
But then it isn't a loop… It is an empty statement: skip, NOP…
