# Formally prove that the loops of this sorting algorithm will terminate [closed]

Given is the sorting algorithm Bubblesort

Bubblesort(A)
for i=1 to A.length
for j=A.length downto i+1
if A[j] < A[j-1]
swap A[j] with A[j-1]


How do you formally prove that the for-loops will terminate?

Can you just argue that A.length is finite, thus the outer loop executes finite, namely A.length times and the inner loop as well just backwards. Thus it's not possible that the inner loop executes more than A.length^2 times and so both for loops will terminate then.

Can you argue like that? But I don't know how you can prove that without using these sentences, make it more formal. Or is this formal already?

## closed as off-topic by Emil Jeřábek, Gamow, Marzio De Biasi, Aryeh, Jan JohannsenDec 17 '18 at 9:02

This question appears to be off-topic. The users who voted to close gave this specific reason:

• "Your question does not appear to be a research-level question in theoretical computer science. For more information about the scope, please see help center. Your question might be suitable for Computer Science which has a broader scope." – Emil Jeřábek, Gamow, Marzio De Biasi, Aryeh, Jan Johannsen
If this question can be reworded to fit the rules in the help center, please edit the question.

Since the loop variables $$i$$ and $$j$$ are not modified in the loop body, you can compute the exact number of iterations. The inner loop is executed $$n-i$$ times in each iteration of the outer loop, so the body of the inner loop is executed exactly $$(n-1)+(n-2)+...+3+2+1 = \frac{n*(n-1)}{2}$$ times, where $$n$$ is the length of the array $$A$$. So the algorithm always terminates.

This should be formal enough. A more complicated proof is only necessary, if the loop variables could be modified in the body under certain conditions. In this case you would have to argue that the particular modifications that are possible cannot cause the loop to run forever.