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