Given is the sorting algorithm Bubblesort

    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?


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.

| cite | improve this answer | |

Not the answer you're looking for? Browse other questions tagged or ask your own question.