En informática teórica , un algoritmo es correcto con respecto a una especificación si se comporta según lo especificado. Lo mejor explorado es la corrección funcional , que se refiere al comportamiento entrada-salida del algoritmo (es decir, para cada entrada produce una salida que satisface la especificación). [1]
Dentro de esta ú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 requiere además que finalmente se devuelva una respuesta, es decir, que el algoritmo termine. En consecuencia, para demostrar la corrección total de un programa, basta con probar su corrección parcial y su terminación. [2] El último tipo de prueba ( prueba de terminación ) nunca puede automatizarse completamente, ya que el problema de la detención es indecidible .
Por ejemplo, buscando sucesivamente entre los números enteros 1, 2, 3,... para ver si podemos encontrar un ejemplo de algún fenómeno (por ejemplo, un número perfecto impar ), es bastante fácil escribir un programa parcialmente correcto (consulte el recuadro). Pero decir que este programa es totalmente correcto sería afirmar algo que actualmente no se conoce en la teoría de números .
Una prueba tendría que ser 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 determinado que implementa el algoritmo en una máquina determinada. Eso implicaría consideraciones tales como limitaciones en la memoria de la computadora .
Un resultado profundo de la teoría de la prueba , la correspondencia Curry-Howard , establece que una prueba de corrección funcional en lógica constructiva corresponde a un determinado 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.
Las pruebas de software son cualquier actividad destinada a evaluar un atributo o capacidad de un programa o sistema y determinar si cumple con los resultados requeridos. Aunque son cruciales para la calidad del software y ampliamente implementadas por programadores y evaluadores, las pruebas de software siguen siendo un arte, debido a la comprensión limitada de los principios del software. La dificultad en las pruebas de software surge de la complejidad del software: no podemos probar completamente un programa con una complejidad moderada. Probar es más que solo depurar. El propósito de las pruebas puede ser el aseguramiento de la calidad, la verificación y validación o la estimación de la confiabilidad. Las pruebas también se pueden utilizar como métrica genérica. Las pruebas de corrección y las pruebas de confiabilidad son dos áreas principales de las pruebas. Las pruebas de software son una compensación entre presupuesto, tiempo y calidad. [4]