Programación de Ciclos Utilizando el Teorema del Invariante

Ejemplo

// Función que dado un vector devuelve true si alguno de sus elementos es mayor a 0
bool hayMayorACero(vector<int> v){
	int i = 0;
  bool encontre = false;
  int n = v.size();
  while (i < n) {
  // Principio de iteración
    encontre = encontre || v[i] > 0;
    i = i + 1;
  // Final de iteración
  }
  return encontre;
}

• Sea v = {-1, 2, -3}

Principio de Iteración

Final de Iteración

Invariantes

¿Cómo sabemos si un invariante es adecuado?

• $P_C \implies I$
• $I \land \lnot B \implies Q_C$
• Vale el invariante al principio y al final de cada iteración
• El invariante debe hacer afirmaciones sobre el acumulador e incluir el rango de la variable de control del ciclo.

Estas cosas no alcanzan para probar que nuestro invariante es correcto para demostrar al correctitud parcial del ciclo pero nos serán útiles para descubrir errores.