Regla 0x1016h: Documentá el invariante de cada lazo

0x1016h: Documentá el invariante de cada lazo¶

Enunciado normativo¶

Todo lazo que no sea evidentemente trivial DEBE documentar, en un comentario inmediatamente anterior, el invariante: qué propiedad se cumple al inicio y al final de cada iteración. La condición de corte y la inicialización deben ser coherentes con ese invariante.

¿Por qué existe esta regla?¶

El problema¶

Los errores en los lazos son los más frecuentes en un curso introductorio: empezar en 1 en vez de 0, terminar en <= en vez de <, olvidar procesar el último elemento. La causa casi siempre es la misma: no se declaró explícitamente qué representa el estado del lazo en cada paso.

El invariante es esa declaración. “Al empezar la iteración i, la suma contiene los primeros i elementos” resuelve de golpe el valor inicial (i = 0, suma vacía), la condición (i < n) y el cuerpo (sumar v[i]). Es la técnica formal más barata para razonar sobre bucles.

Consecuencias de violarla¶

Fundamento en la cátedra¶

Es la versión introductoria del método de invariantes de lazo que se formaliza en contratos y verificación deductiva. Se apoya en 0x1003h: Utilizá el lazo for para iteraciones con rango o contador definido y while para lazos controlados por condiciones lógicas (elegir bien el tipo de lazo) y en 0x0201h: Escribí comentarios que expliquen el ‘porqué’, no el ‘qué’ (comentarios de intención).

Alcance y excepciones¶

Aplica a todo lazo for o while no trivial (recorrido con acumulador, búsqueda, transformación). Un lazo de impresión trivial (for i in 0..n printf) puede omitirlo. La documentación puede ser breve: una o dos líneas.

Ejemplos exhaustivos¶

❌ Contraejemplo 1 — Suma sin invariante declarado¶

int suma = 0;
for (int i = 0; i <= n; i++) {
    suma += v[i];
}

Por qué falla: sin haber fijado el invariante, el <= parece razonable pero lee v[n], fuera de límites. El invariante “suma contiene v[0..i-1] al empezar la iteración i” habría forzado i < n.

❌ Contraejemplo 2 — Búsqueda con estado incierto¶

int i = 0;
while (v[i] != buscado) {
    i++;
}

Por qué falla: no hay invariante ni cota; si el valor no está, el lazo lee fuera del arreglo hasta encontrar casualmente el valor en memoria. Falta el invariante “ninguno de v[0..i-1] es igual a buscado” y la cota i < n.

✅ Ejemplo conforme 1 — Suma con invariante¶

/* Invariante: al empezar la iteracion i, suma == v[0] + ... + v[i-1]. */
int suma = 0;
for (size_t i = 0; i < n; i++) {
    suma += v[i];
}
/* Al terminar, suma == v[0] + ... + v[n-1]. */

El invariante determina el inicio (0), la condición (i < n) y la postcondición.

✅ Ejemplo conforme 2 — Búsqueda con invariante y cota¶

/* Invariante: buscado no esta en v[0..i-1]. */
size_t i = 0;
while (i < n && v[i] != buscado) {
    i++;
}

if (i < n) {
    /* encontrado en la posicion i */
} else {
    /* no esta */
}

La cota i < n evita el acceso fuera de límites y permite concluir, al salir, si se encontró o no.

⚠️ Casos límite¶

• Lazos anidados: cada lazo tiene su propio invariante; el interno suele referirse al externo.

• Recorrido en reversa: el invariante debe reflejar el rango ya procesado (v[n-1] hacia abajo).

• Lazos con break: el invariante deja de garantizarse al salir abruptamente; conviene anotar qué se sabe en cada punto de corte.

Cómo detectarla¶

Checklist de autocontrol¶

• ¿Escribí qué propiedad se cumple al inicio de cada iteración?

• ¿La inicialización hace verdadero el invariante antes de entrar?

• ¿La condición de corte y el avance lo conservan?

• ¿Puedo afirmar la postcondición al salir?

Reglas relacionadas¶

• 0x1003h: Utilizá el lazo for para iteraciones con rango o contador definido y while para lazos controlados por condiciones lógicas — elección de for o while.

• 0x0201h: Escribí comentarios que expliquen el ‘porqué’, no el ‘qué’ — comentarios de intención.

• 0x2016h: Escribí el contrato de la función antes de implementarla — contrato de la función que contiene el lazo.

• 0x100Dh: Prohibición de condiciones de parada compuestas complejas en lazos for — condiciones de parada simples.