If you're seeing this message, it means we're having trouble loading external resources on our website.

Si estás detrás de un filtro de páginas web, por favor asegúrate de que los dominios *.kastatic.org y *.kasandbox.org estén desbloqueados.

Contenido principal

Verificar un algoritmo

Un aspecto importante de cualquier algoritmo es que sea correcto: siempre produce la salida esperada para el rango de entradas y termina en algún momento.
Resulta que es dificil probar que un algoritmo sea correcto. Los programadores frecuentemente usan análisis empírico para encontrar fallas en un algoritmo, pero solamente el razonamiento formal puede demostrar que sea totalmente correcto.

Análisis empírico

Un análisis "empírico" es el que se basa en experimentación y observación real de los resultados. En el mundo de los algoritmos, esto quiere decir que el algoritmo debe ser traducido a un lenguaje de programación, y ejecutado en una computadora.
Hagamos un análisis empírico de un algoritmo para encontrar el máximo valor en una lista de números.
Aquí está el pseudocódigo que expresa ese algoritmo:
maxNum ← -1
FOR num IN numbers {
  if (num > maxNum) {
    maxNum ← num
  }
}
A continuación, lo traduciremos al lenguaje JavaScript, dado que podemos ejecutarlo en nuestro editor interactivo aqui en Khan Academy.
var maxNum = -1;
for (var i = 0; i < numbers.length; i++) { 
  if (numbers[i] > maxNum) {
    maxNum = numbers[i];
  }
}
Luego tenemos que alimentar la entrada del algoritmo, y observar como funciona. Para nuestro primer experimento, usemos un arreglo de 4 números, [13, 4, 24, 7], y veamos si produce el máximo, 24.
¡Bravo, funcionó! ¿Podemos declarar que este es un algoritmo perfectamente correcto y seguir adelante con la vida? Me temo que no es tan fácil...
Es hora del experimento #2. Esta vez hagamos que todos los números en el arreglo sean negativos, [-13, -4, -24, -7]. Esta vez, el valor máximo debiera ser -4, el número negativo más pequeño en la lista.
Ay, el código produjo -1 en vez de -4. Esto es porque el valor inicial de maxNum es -1, y el bucle nunca encuentra un valor en la lista que sea más grande que este. Nuestro algoritmo definitivamente no funciona correctamente para números negativos.
En este punto, necesitamos modificar nuestro algoritmo y hacer un análisis empírico del algoritmo (esperemos) mejorado. Ensayemos una versión del algoritmo que inicializa maxNum al primer número de la lista:
¡Funciona! O, al menos, funciona para una lista de números negativos. ¿Funciona todavía para la lista de números positivos? ¿Qué tal para una lista mixta de números positivos y negativos? ¿Qué tal para fracciones? ¿Qué tal para números irracionales? ¡Hay muchas posibilidades por verificar!
Podemos probar más fácilmente envolviendo nuestro algoritmo con un procedimiento, y usar una biblioteca de pruebas para afirmar que la salida de los procedimientos coincide con lo que esperamos. En Khan Academy Program.assertEqual(actual, expected) es un procedimiento simple de prueba que muestra un error cuando la salida obtenida no es igual a la esperada.
A continuación un análisis empírico sobre cuatro listas diferentes:
¡No hay errores ahí! El nuevo algoritmo se ve más correcto que el viejo. ¿Pero es de verdad correcto? No lo sabemos con certeza. De hecho, podríamos hacer muchos más experimentos y aún no lo sabriamos.
El análisis empírico sólo puede usarse para probar que un algoritmo implementado no es correcto, al descubrir entradas para las cuales la salida no es la esperada. Sin embargo, no puede probar que un algoritmo sea correcto.

Razonamiento formal

La única forma de demostrar que un algoritmo sea correcto para todas las entradas posibles es con razonamientos formales o matemáticos.
Una forma de razonamiento es "prueba por inducción", una técnica también usada por los matemáticos para demostrar propiedades de secuencias numéricas.
📝 Consejo para el examen. El examen AP CSP no requiere entender cómo probar algoritmos por inducción. Lo vimos aquí para darte una idea de cómo se podría ver un razonamiento formal, pero AP no espera que los estudiantes entiendan este nivel avanzado de razonamiento matemático.
Una metáfora puede ayudar a entender la inducción. Imagína que tenemos una fila de un millón de dominós perfectamente espaciados. ¿Cómo sabemos que cada dominó caerá cuando hagamos caer el primero? En realidad no necesitamos comprobar ésto para cada dominó individual. Solamente tenemos que probar que 1) el primer domino caerá, y 2) que el hacer caer cualquier dominó dado hará caer el siguiente dominó. Con solo probar estas dos cosas, ¡podemos probar que un millón de dominós caerán!
Ahora apliquemos inducción a un algoritmo. Aquí está el pseudocódigo para un algoritmo que calcula el factorial de un entero positivo.
PROCEDURE calcFactorial(n) {
    factorial ← 1
    i ← 1
    REPEAT UNTIL (i > n) {
        factorial ← factorial * i
        i ← i + 1
    }
    RETURN factorial
}
El factorial de un numero es el producto de ese número por todos los numeros menores que él, hasta 1. Por ejemplo, el factorial de 4, con frecuencia escrito como 4!, es 4×3×2×1=24.
Antes de tomar el camino para probar que este algoritmo calcula correctamente n!, ensayémoslo cuando n es 4. Si el algoritmo funciona, debe retornar 24.
  • Las variables factorial e i empiezan en 1.
  • Como i (1) no es mayor que n (4), entramos en el bucle.
  • Iteración #1: factorial vale 1 (de 1 * 1), i aumenta a 2.
  • Iteración #2: factorial vale 2 (de 1 * 2), i aumenta a 3.
  • Iteración #3: factorial vale 6 (de 2 * 3), i aumenta a 4.
  • Iteración #4: factorial vale 24 (de 6 * 4), i aumenta a 5.
  • En este punto i (5) es mayor que n (4), así que salimos del bucle.
  • El procedimiento retorna el valor 24.
Genial, hemos verificado que el algoritmo calcula el resultado correcto para un solo entero.
Ahora probemos que para todos los enteros positivos, el algoritmo calcula el factorial del entero.
Primero necesitamos probar que el algoritmo termina en algún momento, pues un algoritmo no puede ser considerado correcto si no para. En este algoritmo i empieza en 1 y aumenta en 1 hasta que se convierte en n+1. Entonces, el algoritmo siempre para después de n iteraciones del bucle.
Luego, para probar que este algoritmo produce el factorial, vamos a probar más específicamente una "invariante de bucle", una propiedad del bucle que debe ser siempre verdadera. En este algoritmo, después de pasar por el bucle n veces, factorial debe ser igual a n! e i debe ser igual a n + 1. Eso fue verdad en nuestro recorrido de factorial(4), y ahora intentaremos probar que es verdad para todo entero positivo en general.
Esto requiere probar: 1) el caso base, y 2) la hipótesis de inducción.
Caso base: aquí es donde verificamos que el algoritmo es válido para el primer número en el rango de entradas posibles.
Probamos este algoritmo para los enteros positivos, asi que el caso base es cuando n es 1. Conforme a nuestra invariante de bucle, después de pasar por el bucle 1 vez, factorial debe ser igual a 1! (1) e i debe ser igual a 1 + 1 (2).
Podemos recorrer nuestro algoritmo para calcFactorial(1), similar a lo que hicimos para el número 4:
  • Las variables factorial e i inician en 1.
  • Como i (1) no es mayor que n (1), el algoritmo ingresa al bucle.
  • Iteración #1: factorial vale 1 (de 1 * 1), i aumenta a 2.
  • En este punto i (2) es mayor que n (1), así que el algoritmo sale del bucle.
Nuestra invariante del bucle es válida; factorial almacena 1, e i vale 2.
Con el caso base ya probado, ¡sigamos adelante!
Paso inductivo: aquí es donde demostramos que si funciona para un número arbitrario, también funciona para el número que le sigue.
Comenzamos con la hipótesis de inducción: suponemos que la invariante del bucle es verdadera para algún entero positivo k. Después de pasar por el bucle k veces, factorial debe ser igual a k! e i debe ser igual a k + 1.
A partir de esa premisa, probaremos que la invariante de bucle también es verdadera para k + 1, el numero que sigue de k. Después de pasar por el bucle k + 1 veces, factorial debe ser igual a (k + 1)! e i debe ser igual a (k + 1) + 1.
Para ello, debemos recorrer calcFactorial(k + 1). Podemos usar avance rápido por las primeras k repeticiones, gracias a la hipótesis de inducción.
  • Despues de k repeticiones, factorial vale k! e i vale k + 1.
  • Iteración #k+1: factorial se coloca en k! * (k + 1), i aumenta a k + 2.
  • En este punto i (cuyo valor es k + 2) es mayor que n (cuyo valor es k + 1), así que el algoritmo sale del bucle.
¿Se mantuvo verdadera la invariante de bucle? ¡Sí, se mantiene! La variable factorial contiene k! * (k + 1), que es equivalente a (k + 1)! y la variable i contiene k + 2, que es equivalente a (k + 1) + 1.
Podemos afirmar con certeza que la invariante de bucle es verdadera para todo entero positivo k.
Dado que mostramos antes que el bucle termina despues de n repeticiones, entonces calcFactorial(n) siempre retorna n!. Nuestro algoritmo es correcto, dado que termina y produce la respuesta correcta cuando termina.
La prueba por inducción es una técnica que funciona bien para algoritmos que iteran sobre enteros, y puede probar que un algoritmo siempre produce la salida correcta. Otros estilos de prueba pueden verificar que otros tipos de algoritmos sean correctos, como prueba por contradicción o prueba por agotamiento.
Este nivel de razonamiento formal definitivamente tiene inconvenientes: primero, muchos programadores de computadoras carecen del entrenamiento matemático para verificar con pruebas, y segundo, la prueba se hace fuera del código, asi que la implementación de un algoritmo puede divergir de la version probada del mismo.
La técnica formal más popular para escribir código correcto es usar lenguajes de programación construidos específicamente con demostrabilidad como meta. Las compañías de computación en la nube, como Amazon y Microsoft, usan lenguajes verificables para su infraestructura crítica, ya que no se pueden dar el lujo que falle por errores en sus algoritmos.
En realidad, la mayoría del software es verificado con análisis empírico. Esto se debe en parte al hecho que la mayoría de los programadores carecen del entrenamiento teórico necesario para probar que sus algoritmos sean correctos. Pero también se debe a que el análisis empírico es fácil, y por el hecho que un conjunto de pruebas bien pensadas puede probar que un algoritmo es casi con certeza correcto; y eso con frecuencia es más que suficiente.

🙋🏽🙋🏻‍♀️🙋🏿‍♂️¿Tienes alguna pregunta sobre este tópico? Nos encantaría contestarte; ¡simplemente pregunta en el área de preguntas abajo!

¿Quieres unirte a la conversación?

Sin publicaciones aún.
¿Sabes inglés? Haz clic aquí para ver más discusiones en el sitio en inglés de Khan Academy.