Your intuition is a great starting point. To formalize this, consider denoting by $F(n)$ the number of times the
col-- happens, or equivalently, the total time you waste in the
col starts with the value of $n$, and can go down to up to $0$ with “jumps” of $1$. Its important that we never pass $0$, since it now means the total number of times
col-- can ever happen is at most $n$. Thus, $F(n)=O(n)$.
Now, consider the rest of the code. You have to account for the
for loop, but notice we already counter the
while loop that is in it with the value of $F(n)$, so we need to calculate the complexity only for any other operations. But clearly, they don’t cost us more than $O(n)$ total, and hence we can say that the algorithm has $O(n)$ run-time.
I believe this should be formal enough. If you want to be even more formal, consider:
- Actually proving that
colnever goes lower than $0$
- Writing line numbers in the algorithm, and explaining the total cost of each line (using the same methods as in this proof)