For some algorithms, conversion to a for loop or recursion is awkward because of side effects, and upper bounds on the number of iterations are too loose.
In such a case, treating each iteration independently doesn't work. We need to analyze the whole loop at once. But, in general, this kind of analysis is too hard.
We need something that captures the iteration-by-iteration behavior while also dealing sensibly with side effects.
