En informática teórica , un algoritmo es correcto con respecto a una especificación si se comporta como se especifica. Lo mejor explorado es la corrección funcional , que se refiere al comportamiento de entrada-salida del algoritmo (es decir, para cada entrada produce una salida que satisface la especificación). [1]
Dentro de la última noción, la corrección parcial , que requiere que si se devuelve una respuesta, será correcta, se distingue de la corrección total , que además requiere que finalmente se devuelva una respuesta, es decir, el algoritmo termina. En consecuencia, para probar la corrección total de un programa, es suficiente probar su corrección parcial y su finalización. [2] El último tipo de prueba (prueba de terminación ) nunca puede automatizarse por completo, ya que el problema de detención es indecidible .
Por ejemplo, buscando sucesivamente entre los enteros 1, 2, 3,... para ver si podemos encontrar un ejemplo de algún fenómeno, digamos un número perfecto impar , es bastante fácil escribir un programa parcialmente correcto (ver cuadro). Pero decir que este programa es totalmente correcto sería afirmar algo que actualmente no se conoce en teoría de números .
Una prueba tendría que ser una prueba matemática, suponiendo que tanto el algoritmo como la especificación se den formalmente. En particular, no se espera que sea una afirmación de corrección para un programa dado que implementa el algoritmo en una máquina dada. Eso implicaría consideraciones tales como limitaciones en la memoria de la computadora .
Un resultado profundo en la teoría de la prueba , la correspondencia de Curry-Howard , establece que una prueba de corrección funcional en lógica constructiva corresponde a cierto programa en el cálculo lambda . Convertir una prueba de esta manera se llama extracción de programa .
La lógica de Hoare es un sistema formal específico para razonar rigurosamente sobre la corrección de los programas de computadora. [3] Utiliza técnicas axiomáticas para definir la semántica del lenguaje de programación y argumentar sobre la corrección de los programas a través de afirmaciones conocidas como triples de Hoare.