Generating all permutations

void permutations(int a[], int n, int start)
{
    if (start == n-1) {
        print_array(a, n);
        return;
    }

    // All permutations with a[start] at the beginning.
    permutations(a, n, start+1);

    for (int i = start+1; i < n; ++i) {
        // Now, bring the other elements to the front.
        swap(&a[start], &a[i]);
        permutations(a, n, start+1);
        swap(&a[start], &a[i]);
    }
}

We use a proof by induction on n-start.

(Base case) When start is n-1, the only permutation satisfying the condition in the statement is the array a itself. Since, we just print the array and return in this case, the array remains unmodified. So both conditions of the statement are satisfied.

Note: In the subsequent proof, the expression b[i] refers to the value in a[i] at the beginning of the function. In the intermediate stages of this function, we may have a[i] ≠ b[i] even though they will be eventually equal.

(Inductive case) Let start be k that is less than n-1. So k+1 is at most n-1 and the inductive hypothesis applies. The set of all permutations of a[start..n-1] is the disjoint union of those that begin with b[start], those that begin with b[start+1], and so on until b[n-1]. The first call to permutations correctly prints all (and exactly) those that has b[start] at position start by the inductive hypothesis. Also, the array is unmodified at the end of this call by the inductive hypothesis.

Now, we have to prove that the for loop correctly prints the rest of the permutations. We use a loop invariant to prove this:

Loop invariant: In the beginning of iteration where i is j, where start < j < n, all permutations that begin with b[start] until b[j-1] has already been printed. Moreover, we have the equality a[start..n-1] = b[start..n-1].

(Base case for the loop invariant, initialization) j = start+1. The first call to permutations in the function has already printed all permutations that begin with b[start]. The array is unchanged too as argued previously.

(Inductive case for the loop invariant, preservation) When start + 1 < j < n, we just have to argue that this iteration of the loop prints all permutations that start with b[j]. Indeed, the first statement, brings b[j] to position start (At this point, the value of a is different, it will be restored later). The inductive hypothesis ensures that all permutations with b[j] at position start are printed. At the end of the recursive call in this iteration, by the second condition of the main theorem, we see that all elements are in the same positions at the beginning of the recursive call. In particular, the element at position j is the same as b[start]. The element at position start is b[j]. These are the only two elements in a that are at different places from b (which is a’s initial value). The last swap fixes this satisfying the equality condition of the loop invariant.

(Termination) At termination, we have start = n (This is when the condition of the for is falsified). By the loop invariant, we have printed all permutations that begin with b[start] until b[n-1], which is all permutations required by the main theorem. The second condition of the loop invariant is the same as the second condition of the main theorem. So both conditions are satisfied closing the induction (for the main theorem).