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

<p>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.</p>

CC BY-SA 4.0
2018-12-15T18:13:58.663Z
2018-12-15T18:20:43.320Z
2018-12-15T18:20:43.320Z
Mark Dettinger
<p>Given is the sorting algorithm Bubblesort</p>

<pre><code>Bubblesort(A)
    for i=1 to A.length
        for j=A.length downto i+1
            if A[j] &lt; A[j-1]
                swap A[j] with A[j-1]
</code></pre>

<p>How do you formally prove that the for-loops will terminate?</p>

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

<p>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?  </p>

<ds.algorithms><sorting><proofs>
Formally prove that the loops of this sorting algorithm will terminate
kathelk
# Formally prove that the loops of this sorting algorithm will terminate

(Asked by: username_0 on 2018-12-15)

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?

**Tags:** ds.algorithms, sorting, proofs


---

## 1 answers

### Answer by username_1 on 2018-12-15. Score: 3 | Accepted answer

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.


---

