Ciclo invariante

De manera informal, ciclo invariante es algún predicado o condición que se mantiene en cada iteración de un ciclo. Por ejemplo:

int j = 9;
    for(int i=1; i<10; i++){
        j--;
        int resul=j+i;
        cout<<"i: "<<i<<endl;

        if(resul == 9){
            cout<<"Cumple el invariente de bucle"<<endl;
        }

    }

En este ejemplo se cumple la invariante de ciclo para cada iteración, ya que se mantiene la condición siguiente:

 i + j == 9

Otra invariante más débil es:

i >= 0 && i < 10 //(condición terminal) 
//o bien 
j <= 9 && j >= 0

Las invariantes de ciclo sirven para probar que un algoritmo esté correcto.

Propiedades

Inicialización. Es verdadera desde la primera iteración.

Mantenimiento. Es verdadera después de una iteración del ciclo. Se mantiene verdadera antes de la iteración próxima.

Terminación. Cuando finaliza el ciclo, la invariante aporta una propiedad que indica que el algoritmo es correcto.

Ejemplos

Insertion sort

import java.util.Arrays;
class InsertionSort{
	public static void main(String[]args){
		int[]array={5,2,4,6,1,3};
		String out="";
		out+=Arrays.toString(array)+"\nResult:\n";		
		
		//start
		for(int i=1;i<array.length;i++){
			int key=array[i];
			int j=i-1;
			out+="array["+j+"] > key = "+array[j] +" > "+key+" = "+(array[j]>key)+"\n";
			while(j>=0 && array[j]>key ){
				array[j+1]=array[j];out+=" \tarray["+j+"+1]=array["+j+"]\n";
				j--;
			}
				array[j+1]=key;
		
		}
		out+=Arrays.toString(array)+"\n";
		
		System.out.println(out);
	}
}

Referencias

Introduction to Algorithms. Third Edition. Thomas H. Cormen. 2009.

https://web.archive.org/web/20130721040913/http://espacio.redsaltillo.net/programacion/insertionsort-algorithm

Datos: Q2238838