Correctness and the Loop Invariant

Loop Invariant
In computer science, you could prove it formally with a loop invariant, where you state that the desired property is maintained in your loop. Such proof is broken down into the following parts:

1.Initialization: It is true (in a limited sense) before the loop runs.

2.Maintenance: If it's true before an iteration of a loop, it remains true before the next iteration.

3.Termination: It will terminate in a useful way once it is finished.

Example:

Input:  n=6, arr[]={7,4,3,5,6,2}
Output: 2 3 4 5 6 7 

Approach

Java

public class CorrectnessLoopInvariant {
    public static void main(String[] args) {
        int arr[] = { 7, 4, 3, 5, 6, 2 };
        insertionSort(arr);
    }

    public static void insertionSort(int[] arr) {
        int n = arr.length;

        for (int i = 1; i < n; i++) {
            int x = arr[i];
            int j = i;
            while (j > 0 && arr[j - 1] > x) {
                arr[j] = arr[j - 1];
                j--;
            }
            arr[j] = x;
        }
        for (int i = 0; i < n; i++) {
            System.out.print(arr[i] + " ");
        }
    }
}

C++

#include <bits/stdc++.h>
using namespace std;

int main()
{
    int n = 6;
    int arr[n] = {7, 4, 3, 5, 6, 2};

    for (int i = 1; i < n; i++)
    {
        int x = arr[i];
        int j = i;
        while (j > 0 && arr[j - 1] > x)
        {
            arr[j] = arr[j - 1];
            j--;
        }
        arr[j] = x;
    }
    for (int i = 0; i < n; i++)
        cout << arr[i] << " ";
    return 0;
}