Correctness and the Loop Invariant


Problem Statement :


In the previous challenge, you wrote code to perform an Insertion Sort on an unsorted array. But how would you prove that the code is correct? I.e. how do you show that for any input your code will provide the right output?

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

Initialization: It is true (in a limited sense) before the loop runs.
Maintenance: If it's true before an iteration of a loop, it remains true before the next iteration.
Termination: It will terminate in a useful way once it is finished.

Insertion Sort's Invariant
Say, you have some InsertionSort code, where the outer loop goes through the whole array : A.

for(int i = 1; i < A.length; i++){
//insertion sort code
You could then state the following loop invariant:

At the start of every iteration of the outer loop (indexed with ), the subarray until  consists of the original elements that were there, but in sorted order.



To prove Insertion Sort is correct, you will then demonstrate it for the three stages:

Initialization - The subarray starts with the first element of the array, and it is (obviously) sorted to begin with.

Maintenance - Each iteration of the loop expands the subarray, but keeps the sorted property. An element  gets inserted into the array only when it is greater than the element to its left. Since the elements to its left have already been sorted, it means  is greater than all the elements to its left, so the array remains sorted. (In Insertion Sort 2 we saw this by printing the array each time an element was properly inserted.)

Termination - The code will terminate after  has reached the last element in the array, which means the sorted subarray has expanded to encompass the entire array. The array is now fully sorted.




You can often use a similar process to demonstrate the correctness of many algorithms. You can see these notes for more information.

Challenge

In the InsertionSort code below, there is an error. Can you fix it? Print the array only once, when it is fully sorted.

Input Format

There will be two lines of input:

 s - the size of the array
arr - the list of numbers that makes up the array


Output Format

Output the numbers in order, space-separated on one line.


Solution :



title-img 


                            Solution in C :

In   C++  :







#include <stdio.h>
#include <string.h>
#include <math.h>
#include <stdlib.h>
#include <assert.h>
/* Head ends here */
void insertionSort(int ar_size, int *  ar) {    
    int i,j;
    int value;
    for(i=1;i<ar_size;i++)
    {
        value=ar[i];
        j=i-1;
        while(j>=0 && value<ar[j])
        {
            ar[j+1]=ar[j];
            j=j-1;
        }
        ar[j+1]=value;        
    }
   for(j=0;j<ar_size;j++)
        {
            printf("%d",ar[j]);
            printf(" ");
        }
}
/* Tail starts here */
int main(void) {
   
   int _ar_size;
scanf("%d", &_ar_size);
int _ar[_ar_size], _ar_i;
for(_ar_i = 0; _ar_i < _ar_size; _ar_i++) { 
   scanf("%d", &_ar[_ar_i]); 
}

insertionSort(_ar_size, _ar);
   
   return 0;
}









In   Java  :






import java.io.*;
import java.util.*;

public class Solution {
    
    public static void insertionSort(int[] A){
      for(int i = 1; i < A.length; i++){
        int value = A[i];
        int j = i - 1;
        while(j >= 0 && A[j] > value){
          A[j + 1] = A[j];
          j = j - 1;
        }
        A[j + 1] = value;
      }
        
        printArray(A);
}

    
    static void printArray(int[] ar) {
         for(int n: ar){
            System.out.print(n+" ");
         }
      }
/* Tail starts here */
public static void main(String[] args) {
           Scanner in = new Scanner(System.in);
           int n = in.nextInt();
           int[] ar = new int[n];
           for(int i=0;i<n;i++){
              ar[i]=in.nextInt(); 
           }
           insertionSort(ar);
       }    
   }









In   C  :








#include <stdio.h>
#include <string.h>
#include <math.h>
#include <stdlib.h>
#include <assert.h>
/* Head ends here */
#include <stddef.h>
void insertionSort(int ar_size, int *  ar) {    
    int i,j;
    int value;
    for(i=1;i<ar_size;i++)
    {
        value=ar[i];
        j=i-1;
        while(j>=0 && value<ar[j])
        {
            ar[j+1]=ar[j];
            j=j-1;
        }
        ar[j+1]=value;        
    }
    for(j=0;j<ar_size;j++)
        {
            printf("%d",ar[j]);
            printf(" ");
        }
}
/* Tail starts here */
int main(void) {   
   int _ar_size;
scanf("%d", &_ar_size);
int _ar[_ar_size], _ar_i;
for(_ar_i = 0; _ar_i < _ar_size; _ar_i++) { 
   scanf("%d", &_ar[_ar_i]); 
}

insertionSort(_ar_size, _ar);
   
   return 0;
}









In   Python3  :






num_integers = int(input())
str_in = [int(x) for x in input().strip().split(' ')]
print(' '.join([str(x) for x in sorted(str_in)]))








View More Similar Problems

Tree: Huffman Decoding

Huffman coding assigns variable length codewords to fixed length input characters based on their frequencies. More frequent characters are assigned shorter codewords and less frequent characters are assigned longer codewords. All edges along the path to a character contain a code digit. If they are on the left side of the tree, they will be a 0 (zero). If on the right, they'll be a 1 (one). Only t

View Solution →

Binary Search Tree : Lowest Common Ancestor

You are given pointer to the root of the binary search tree and two values v1 and v2. You need to return the lowest common ancestor (LCA) of v1 and v2 in the binary search tree. In the diagram above, the lowest common ancestor of the nodes 4 and 6 is the node 3. Node 3 is the lowest node which has nodes and as descendants. Function Description Complete the function lca in the editor b

View Solution →

Swap Nodes [Algo]

A binary tree is a tree which is characterized by one of the following properties: It can be empty (null). It contains a root node only. It contains a root node with a left subtree, a right subtree, or both. These subtrees are also binary trees. In-order traversal is performed as Traverse the left subtree. Visit root. Traverse the right subtree. For this in-order traversal, start from

View Solution →

Kitty's Calculations on a Tree

Kitty has a tree, T , consisting of n nodes where each node is uniquely labeled from 1 to n . Her friend Alex gave her q sets, where each set contains k distinct nodes. Kitty needs to calculate the following expression on each set: where: { u ,v } denotes an unordered pair of nodes belonging to the set. dist(u , v) denotes the number of edges on the unique (shortest) path between nodes a

View Solution →

Is This a Binary Search Tree?

For the purposes of this challenge, we define a binary tree to be a binary search tree with the following ordering requirements: The data value of every node in a node's left subtree is less than the data value of that node. The data value of every node in a node's right subtree is greater than the data value of that node. Given the root node of a binary tree, can you determine if it's also a

View Solution →

Square-Ten Tree

The square-ten tree decomposition of an array is defined as follows: The lowest () level of the square-ten tree consists of single array elements in their natural order. The level (starting from ) of the square-ten tree consists of subsequent array subsegments of length in their natural order. Thus, the level contains subsegments of length , the level contains subsegments of length , the

View Solution →