Facundo Uferer
La Tripleta de Hoare {P} C {Q}: El Contrato Matemático
Si la precondición P es verdadera antes de ejecutar el bloque C, entonces la postcondición Q será indefectiblemente verdadera al terminar. Es el contrato formal entre una especificación y su implementación.
valores != null && length > 0 Esperando prueba… maximoActual = maximo(valores) Inactivo ∀x ∈ valores: x ≤ maximoActual Esperando prueba… Invariantes de Bucle: El Estado que Nunca se Rompe
Un invariante es una afirmación lógica verdadera antes de iniciar el bucle, al final de cada iteración y al terminar, garantizando la postcondición. En maximo(), dice: valores[0..i-1] ya fue recorrido y maximoActual es su máximo.
Antes de empezar: el segmento [0..-1] está vacío, el invariante se cumple trivialmente.
Corrección Total y Función Cota: V = n − i
La corrección parcial garantiza que, si el bucle termina, la respuesta es correcta. La corrección total exige además que termine: una función cota entera y positiva que decrece estrictamente en cada iteración lo demuestra.
V comienza en n = 8. Cada iteración lo reduce en 1. Mientras V sea positivo, el bucle puede seguir; nunca puede volverse negativo.
El Gráfico Interactivo de la Notación Big-O
Big-O describe cómo escala el tiempo de ejecución cuando el tamaño de entrada N crece hacia el infinito, ignorando constantes y términos menores para enfocarse en el factor dominante.
Mejor, Peor y Caso Promedio en una Búsqueda Lineal
Un algoritmo no tiene una única velocidad: la búsqueda lineal es O(1) en el mejor caso si el valor está al principio, y O(N) en el peor caso si no existe. Sin aclaración, suele informarse el peor caso.
Buscando el valor 12 en el arreglo: