Una fórmula que falla en el caso 41
Probar un programa es ejecutarlo con unos datos y mirar si el resultado es el esperado. Una demostración va más lejos: garantiza el resultado para todos los casos posibles, no solo para los que probaste.
Una secretaría quiere que el código de cada matrícula sea un número primo. Calcula el código con n * n + n + 41 y lo prueba con los primeros 40 números. Los 40 códigos salen primos. El número 41 da uno que no lo es.
Al final de esta lección
Nota
Puedo explicar qué garantiza una prueba y qué garantiza una demostración.
Palabras clave
| Palabra | Qué significa | Ejemplo |
|---|---|---|
| Prueba | ejecutar el programa con unos datos concretos | |
| Caso | un valor o una situación concreta | |
| Afirmación | algo que debe ser cierto siempre | el código es primo |
| Contraejemplo | un caso que demuestra que la afirmación es falsa | |
| Demostración | un argumento que vale para todos los casos | |
| Método formal | una técnica en la que una máquina comprueba todos los casos |
Las celdas que rellenan los estudiantes quedan en blanco en esta vista previa.
Una prueba solo mira los casos que eliges
Cada prueba responde a una pregunta pequeña: ¿funciona con este dato? Si pasa, sabes que funciona con ese dato y con ninguno más.
Cuantas más pruebas haces, más confías. Pero la confianza no es una garantía: un caso que no probaste puede fallar.
Ejemplo: los códigos de matrícula
| n | n * n + n + 41 | ¿Es primo? |
|---|---|---|
| 0 | 41 | Sí |
| 1 | 43 | Sí |
| 2 | 47 | Sí |
| 10 | 151 | Sí |
| 39 | 1601 | Sí |
| 40 | 1681 | No: es 41 por 41 |
Las celdas que rellenan los estudiantes quedan en blanco en esta vista previa.
Prueba los primeros 40 números
python3 -c "print(all(all((n*n+n+41) % d != 0 for d in range(2, n*n+n+41)) for n in range(40)))"Se muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Prueba un número más
python3 -c "print(all(all((n*n+n+41) % d != 0 for d in range(2, n*n+n+41)) for n in range(41)))"Se muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Un contraejemplo basta para refutar
Para demostrar que una afirmación es falsa, no hacen falta miles de casos. Basta uno: el contraejemplo.
Para demostrar que es cierta pasa lo contrario. Ni un millón de casos buenos lo garantizan. Hay que argumentar sobre todos a la vez, y eso es lo que hace un método formal.
Un error frecuente
Advertencia
Mucha gente cree que, si una afirmación pasa muchísimas pruebas, ya está demostrada. No lo está. Cada prueba solo cubre su caso. Una afirmación se da por demostrada cuando se argumenta sobre todos los casos, o se refuta con un solo contraejemplo.
Una máquina revisa todos los casos
Hay infinitos números enteros, y nadie los prueba uno a uno. Un solver es un programa que razona sobre todos a la vez.
Z3 es uno de ellos. Los dos Runs siguientes le dan una afirmación sobre un entero x y le piden un caso donde falle. Si responde unsat, no existe ese caso: la afirmación vale para todos los enteros. Si responde sat, existe, y es un contraejemplo.
¿Falla x * x >= x en algún entero?
echo '(declare-const x Int) (assert (not (>= (* x x) x))) (check-sat)' | z3 -inSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
¿Falla x * x > x en algún entero?
echo '(declare-const x Int) (assert (not (> (* x x) x))) (check-sat)' | z3 -inSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Cuándo merece la pena un método formal
Un método formal cuesta más esfuerzo que una prueba. Compensa cuando fallar sale caro y los casos son demasiados para probarlos.
Dos ejemplos: un pago que dos procesos modifican a la vez, o una regla que debe cumplirse con cualquier entero. En las cinco lecciones siguientes usarás cuatro herramientas para esos casos: Z3, SPIN, TLA+ y Alloy.