Contenido principal
Principios de ciencias de la computación avanzados (AP Computer Science Principles)
Curso: Principios de ciencias de la computación avanzados (AP Computer Science Principles) > Unidad 4
Lección 2: Evaluación de algoritmosVerificar 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, times, 3, times, 2, times, 1, equals, 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
ei
empiezan en1
. - Como
i
(1
) no es mayor quen
(4
), entramos en el bucle. - Iteración #1:
factorial
vale1
(de1 * 1
),i
aumenta a2
. - Iteración #2:
factorial
vale2
(de1 * 2
),i
aumenta a3
. - Iteración #3:
factorial
vale6
(de2 * 3
),i
aumenta a4
. - Iteración #4:
factorial
vale24
(de6 * 4
),i
aumenta a5
. - En este punto
i
(5
) es mayor quen
(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
ei
inician en1
. - Como
i
(1
) no es mayor quen
(1
), el algoritmo ingresa al bucle. - Iteración #1:
factorial
vale1
(de1 * 1
),i
aumenta a2
. - En este punto
i
(2
) es mayor quen
(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
valek!
ei
valek + 1
. - Iteración #
k+1
:factorial
se coloca enk! * (k + 1)
,i
aumenta ak + 2
. - En este punto
i
(cuyo valor esk + 2
) es mayor quen
(cuyo valor esk + 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.