Invariantes de ciclo¶
Grupo B — viernes 21 de agosto de 2026.
Nota en preparación
El texto de esta nota se publica después de la clase. Los ejercicios interactivos ya están disponibles y se pueden trabajar desde ya.
La especificación de un problema¶
Invariantes de ciclo¶
La demostración completa: el factorial¶
Segundo ejemplo: búsqueda en un arreglo¶
Ejercicios¶
Ejercicios interactivos¶
Dos ejercicios en el navegador siguen el camino completo de la clase: ver el patrón en la traza, nombrarlo como la pareja de invariantes I₀ e I₁ y armar la demostración por inicialización y estabilidad. Están en la página de ejercicios interactivos:
- sumar — el primer
ciclo de la clase: descubra qué se conserva en la traza de
sumarArreglo, nombre I₀ e I₁ y complete la demostración del Teorema 1 hasta el Teorema 2. - factorial — el
mismo recorrido con menos ayuda y la condición
i <= N, que cambia las cotas. Cierra con el experimento defact(-1): fuera de la precondición no hay promesa.