Para comprobar la corrección de un programa informático, a menudo nos limitamos a probarlo mediante una batería de pruebas, lo cual solo es suficiente si se prueban todos los casos posibles. Antes de llegar a esta etapa, conviene construir el programa a partir de su demostración. En realidad, el problema solo se plantea en el caso de los bucles iterativos o recursivos.
Referencias
La lógica. Bibliothèque Tangente 15, 2004.
Matemáticas e informática. Bibliothèque Tangente 52, 2014.
Las demostraciones. Bibliothèque Tangente 55, 2015.

Sucesión de 11 (18). Bernard Frize, 2006.

-
Más delicado: el caso de las funciones iterativas ----------------------------------------------
En general, resulta más difícil demostrar que un programa proporciona el resultado esperado para una función iterativa (es decir, estructurada en torno a un bucle como «repetir», «mientras» o «para») que para una función recursiva. Las demostraciones se basan en la noción de invariante de bucle.
Veamos el caso del cálculo del MCD (máximo común divisor) de dos números mediante el algoritmo de Euclides. La brillante idea atribuida a Euclides consiste en observar que el MCD de dos números a y b es el mismo que el de a y b módulo a, es decir, el resto d de la división euclídea de a entre b. Tenemos entonces el siguiente programa en pseudocódigo:
Mcd(a,b)=
Introducimos una variable adicional d
Repetir
d:=a mod b
a:=b
b:=d
hasta que d=0
devolver a
El invariante de bucle es: «Los divisores comunes de a y b son los mismos en cada etapa». Por otra parte, la sucesión de valores de d es estrictamente decreciente, lo que garantiza la salida del bucle. Este algoritmo puede expresarse de forma recursiva:
McdRec(a,b)=
Si a=0, devolver b
En caso contrario, devolver McdRec(b mod a, a)
Este programa se demuestra entonces sin dificultad por inducción sobre el número entero a.
-
Programar es demostrar: el caso de las funciones recursivas -----------------------------------------------------------
El cuerpo de una función recursiva consta por lo general de dos partes: el tratamiento del caso base y la parte propiamente recursiva, lo que guarda relación con el razonamiento por inducción. El ejemplo clásico es el cálculo del factorial de un número entero positivo. He aquí un ejemplo en pseudocódigo:
Factorial(n)=
Si n=0, devolver 1
En caso contrario, devolver n\*Factorial(n-1)
La demostración de que la función Factorial devuelve efectivamente el producto de todos los números enteros de 1 a n (denotado n!) para todo número natural n se realiza por inducción. La demostración se realiza leyendo las líneas del programa anterior. Formalicemos el razonamiento considerando P(n) como la propiedad «Factorial(n) devuelve n!».
P(0) es verdadera según la primera línea del programa. Supongamos ahora que P(n–1) es verdadera para un número entero n ≥ 1 y examinemos P(n). Factorial(n) llama a Factorial(n-1), que, según la hipótesis de inducción, devuelve (n–1)!. Por tanto, la segunda línea del programa devuelve n×(n–1)!, que vale n!, de modo que P(n) es verdadera. Así pues, P(0) es verdadera y, si P(n–1) es verdadera, P(n) también lo es. Por el principio de inducción, P(n) es, por tanto, verdadera para todo número natural n.
En realidad, esta demostración sigue exactamente la programación de la función. Podemos resumirlo afirmando que, en este caso, ¡programar es demostrar!