Condición invariante de bucle con ejemplos

Definición:

Una invariante de bucle es una condición [entre las variables de programa] que necesariamente se cumple inmediatamente antes e inmediatamente después de cada iteración de un bucle. (Tenga en cuenta que esto no dice nada acerca de su verdad o falsedad en medio de una iteración).

Un bucle invariante es un predicado (condición) que se cumple para cada iteración del bucle.

Por ejemplo, veamos un bucle for simple que se ve así:

int j = 9;
for(int i=0; i<10; i++)  
j--;

En este ejemplo es cierto (para cada iteración) que i + j == 9.

Un invariante más débil que también es cierto es que i >= 0 && i <= 10.

Uno puede confundirse entre el bucle invariante y el bucle condicional (la condición que controla la terminación del bucle).

El bucle invariante debe ser verdadero:

• antes de que comience el bucle
• antes de cada iteración del ciclo
• después de que el ciclo termina

(aunque puede ser falso temporalmente durante el cuerpo del bucle).

Por otro lado, el bucle condicional debe ser falso después de que termine el bucle, de lo contrario, el bucle nunca terminaría.

Uso:

Los bucles invariantes capturan hechos clave que explican por qué funciona el código. Esto significa que si escribe código en el que la invariancia del ciclo no es obvia, debe agregar un comentario que proporcione la invariancia del ciclo. Esto ayuda a otros programadores a comprender el código y ayuda a evitar que rompan accidentalmente el invariante con cambios futuros.

Un ciclo invariante puede ayudar en el diseño de algoritmos iterativos cuando se considera una afirmación que expresa relaciones importantes entre las variables que deben ser verdaderas al comienzo de cada iteración y cuando termina el ciclo. Si esto se mantiene, el cómputo está en camino a la efectividad. Si es falso, entonces el algoritmo ha fallado.

Los invariantes de bucle se utilizan para razonar sobre la corrección de los programas de computadora. Se puede usar la intuición o el ensayo y error para escribir algoritmos sencillos; sin embargo, cuando aumenta la complejidad del problema, es mejor usar métodos formales como invariantes de bucle.

Las invariantes de bucle se pueden usar para probar la corrección de un algoritmo, depurar un algoritmo existente sin siquiera rastrear el código o desarrollar un algoritmo directamente a partir de la especificación.

Un buen bucle invariante debe satisfacer tres propiedades:

• Inicialización: la invariante del bucle debe ser verdadera antes de la primera ejecución del bucle.
• Mantenimiento: si el invariante es verdadero antes de una iteración del bucle, también debería serlo después de la iteración.
• Terminación: cuando el bucle termina, el invariante debería decirnos algo útil, algo que nos ayude a comprender el algoritmo.

Condición 
invariable del bucle: La condición invariable del bucle es una condición sobre la relación entre las variables de nuestro programa que es definitivamente cierta inmediatamente antes e inmediatamente después de cada iteración del bucle. 
Por ejemplo: Considere una array A{7, 5, 3, 10, 2, 6} con 6 elementos y tenemos que encontrar el máximo de elementos en la array. 

max = -INF (minus infinite)
for (i = 0 to n-1)
  if (A[i] > max)
      max = A[i]

En el ejemplo anterior, después de la tercera iteración del bucle, el valor máximo es 7, lo que es cierto para los primeros 3 elementos de la array A. Aquí, la condición invariable del bucle es que el máximo siempre es máximo entre los primeros i elementos de la array A. 

Condición invariable de bucle de varios algoritmos: 
requisito previo : ordenación por inserción , ordenación por selección , ordenación rápida , ordenación por burbujas , búsqueda binaria

Clasificación de selección: 
en el algoritmo de clasificación de selección , encontramos el elemento mínimo de la parte no clasificada y lo colocamos al principio. 

min_idx = 0
 
for (i = 0; i < n-1; i++)
{
   min_idx = i;
   for (j = i+1 to n-1)
      if (arr[j] < arr[min_idx])
         min_idx = j;

    swap(&arr[min_idx], &arr[i]);
}

En el pseudocódigo anterior hay dos condiciones invariantes de bucle: 

1. En el ciclo externo, la array se ordena para los primeros elementos i.
2. En el ciclo interno, min es siempre el valor mínimo en A[i a j].

Ordenación por inserción: 
en la ordenación por inserción , la condición invariable del ciclo es que el subarreglo A[0 a i-1] siempre está ordenado. 

for (i = 1 to n-1)
{
   key = arr[i];
   j = i-1;
   while (j >= 0 and arr[j] > key)
   {
      arr[j+1] = arr[j];
      j = j-1;
   }
   arr[j+1] = key;
}

Ordenación rápida: 
en el algoritmo de ordenación rápida , después de que cada array de llamada de partición se divida en 3 regiones: 

1. El elemento de pivote se coloca en su posición correcta.
2. Los elementos menores que el elemento pivote se encuentran en el lado izquierdo del elemento pivote.
3. Los elementos mayores que el elemento pivote se encuentran en el lado derecho del elemento pivote.

quickSort(arr[], low, high)
{
    if (low < high)
    {
        pi = partition(arr, low, high);
        quickSort(arr, low, pi - 1);  // Before pi
        quickSort(arr, pi + 1, high); // After pi
    }
}

partition (arr[], low, high)
{
    pivot = arr[high];   
    i = (low - 1) 
    for (j = low; j <= high- 1; j++)
        if (arr[j] <= pivot)
            i++;   
            swap arr[i] and arr[j]
    swap arr[i + 1] and arr[high])
    return (i + 1)
}

Ordenamiento de burbuja: 

En el algoritmo de clasificación de burbujas , después de cada iteración del ciclo, el elemento más grande de la array siempre se coloca en la posición más a la derecha. Por lo tanto, la condición invariante del bucle es que al final de la iteración i, la mayoría de los elementos i están ordenados y en su lugar.  

for (i = 0 to n-1)         
  for (j = 0 to j  arr[j+1])
       swap(&arr[j], &arr[j+1]);

Encuentre el índice del valor mínimo en una array de enteros:

Tenemos una array A, que tiene n elementos en ella. Mantenemos dos variables, nextToCheck ysmallestSoFar. Inicialmente establecemos el valor más pequeño hasta ahora en 0 y comparamos A[1], A[2], …, A[n-1] con A[más pequeño hasta ahora]. Si la comparación actual muestra un valor más pequeño, actualizamos el valor más pequeño hasta ahora.

Aquí está el bucle invariante:

smallestSoFar in [0,nextToCheck),
and for all k in [0,nextToCheck), A[k] >= A[smallestSoFar].

[a,b) significa todos los números enteros de a a b, incluyendo a, pero sin incluir b.

Establecemos el bucle invariante verdadero antes del bucle configurando:

nextToCheck = 1 ;
smallestSoFar = 0 ;

Cada vez que recorremos el bucle, incrementamos nextToCheck en uno y arreglamos más pequeño hasta ahora para mantener el Loop Invariant verdadero:

 if ( a[smallestSoFar] > a[nextToCheck] ) {
    smallestSoFar = nextToCheck ;
 }
 nextToCheck ++ ;

La condición de finalización es nextToCheck==n, es decir, no hay más que comprobar.

La combinación de la invariante de bucle y la condición de terminación da quesmallSoFar es el índice del valor más pequeño de la array.

Búsqueda binaria:

bsearch(type A[], type a) {
start = 1, end = length(A)

  while ( start <= end ) {
      mid = floor(start + end / 2)

      if ( A[mid] == a ) return mid
      if ( A[mid] > a ) end = mid - 1
      if ( A[mid] < a ) start = mid + 1

  }
  return -1

}

El invariante es el enunciado lógico:

if ( A[mid] == a ) then ( start <= mid <= end )

Esta declaración es una tautología lógica: siempre es cierta en el contexto del ciclo/algoritmo específico que estamos tratando de probar. Y proporciona información útil sobre la corrección del ciclo después de que finaliza.

Si regresamos porque encontramos el elemento en la array, entonces la declaración es claramente verdadera, ya que si A[mid] == a entonces a está en la array y mid debe estar entre el inicio y el final. Y si el bucle termina porque inicio > fin, entonces no puede haber un número tal que inicio <= medio y medio <= fin y, por lo tanto, sabemos que la afirmación A[medio] == a debe ser falsa. Sin embargo, como resultado, el enunciado lógico general sigue siendo verdadero en el sentido nulo. (En lógica, la afirmación si (falso) entonces (algo) siempre es verdadera.)