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=0; i<10; i++) j--; 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.