En informática teórica , la corrección de un algoritmo se afirma cuando se dice que el algoritmo es correcto con respecto a una especificación . La corrección funcional se refiere al comportamiento de entrada-salida del algoritmo (es decir, para cada entrada produce la salida esperada). [1]
Se hace una distinción entre corrección parcial , que requiere que si se devuelve una respuesta sea correcta, y corrección total , que además requiere que el algoritmo finalice. Dado que no existe una solución general para el problema de la detención , la corrección total no es decidible . Una prueba de terminación es un tipo de prueba matemática que juega un papel crítico en la verificación formal porque la corrección total de un algoritmo depende de la terminación. [2]
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 (usando factorización para calcular la alícuota de cada entero suma ). 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 una prueba matemática, asumiendo que tanto el algoritmo como la especificación se dan 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 determinada. 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 Curry-Howard , establece que una prueba de corrección funcional en lógica constructiva corresponde a un cierto programa en el cálculo lambda . La conversión de una prueba de esta forma se denomina 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.
La prueba de software es cualquier actividad destinada a evaluar un atributo o capacidad de un programa o sistema y determinar que cumple con los resultados requeridos. Aunque es crucial para la calidad del software y es ampliamente implementado por programadores y probadores, 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 se debe a la complejidad del software: no podemos probar completamente un programa con una complejidad moderada. Probar es más que depurar. El propósito de las pruebas puede ser garantía de calidad, verificación y validación o estimación de confiabilidad. Las pruebas también se pueden utilizar como métrica genérica. Las pruebas de exactitud y confiabilidad son dos áreas principales de prueba. Las pruebas de software son un compromiso entre presupuesto, tiempo y calidad. [4]
Ver también
Notas
- ^ Dunlop, Douglas D .; Basili, Victor R. (junio de 1982). "Un análisis comparativo de corrección funcional" . Comunicaciones de la ACM . 14 (2): 229–244. doi : 10.1145 / 356876.356881 .
- ^ Maná, Zohar; Pnueli, Amir (septiembre de 1974). "Aproximación axiomática a la corrección total de los programas". Acta Informatica . 3 (3): 243–263. doi : 10.1007 / BF00288637 .
- ^ Hoare, CAR (octubre de 1969). "Una base axiomática para la programación informática" (PDF) . Comunicaciones de la ACM . 12 (10): 576–580. CiteSeerX 10.1.1.116.2392 . doi : 10.1145 / 363235.363259 . Archivado desde el original (PDF) el 4 de marzo de 2016.
- ^ Pan, Jiantao (primavera de 1999). "Pruebas de software" (cursos). Universidad Carnegie Mellon . Consultado el 21 de noviembre de 2017 .
Referencias
- " Tecnología del lenguaje humano. Desafíos para la informática y la lingüística ". Libros de Google. Np, nd Web. 10 de abril de 2017.
- " Seguridad en Computación y Comunicaciones ". Libros de Google. Np, nd Web. 10 de abril de 2017.
- " El problema de la detención de Alan Turing: una explicación muy alegre e ilustrada ". El problema de la detención de Alan Turing: una explicación muy alegre e ilustrada. Np, nd Web. 10 de abril de 2017.
- Turner, Raymond y Nicola Angius. " La filosofía de la informática ". Enciclopedia de Filosofía de Stanford . Universidad de Stanford, 20 de agosto de 2013. Web. 10 de abril de 2017.
- Dijkstra, EW "Corrección del programa". Universidad de Texas en Austin, Departamentos de Matemáticas y Ciencias de la Computación, Proyecto de prueba automática de teoremas, 1970. Web.