Cicle invariante

De manera informal, cicle invariante és algun predicat o condició que es manté en cada iteración d'un cicle. Per eixemple:

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

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

    }

En este eixemple es complix l'invariante de cicle per a cada iteración, ya que es manté la condició següent:

 i + j == 9

Una atra invariante més dèbil és:

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

Les invariantes de cicle servixen per a provar que un algoritme estiga correcte.

Propietats

• Inicialización. És verdadera des de la primera iteración.

• Manteniment. És verdadera despuix d'una iteración del cicle. Es manté verdadera abans de la iteración pròxima.

• Terminació. Quan finalisa el cicle, la invariante aporta una propietat que indica que l'algoritme és correcte.

Eixemples

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)+"
Result:
";		
		
		//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)+"
";
			while(j>=0 && array[j]>key ){
				array[j+1]=array[j];out+=" 	array["+j+"+1]=array["+j+"]
";
				j--;
			}
				array[j+1]=key;
		
		}
		out+=Arrays.toString(array)+"
";
		
		System.out.println(out);
	}
}

Referències

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

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