Corrección (informática)

En informática teórica , un algoritmo es correcto con respecto a una especificación si se comporta como se especifica. El concepto más estudiado es la corrección funcional , que se refiere al comportamiento de entrada-salida del algoritmo: 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, esta sea correcta, se distingue de la corrección total , que además requiere que finalmente se devuelva una respuesta , es decir, que el algoritmo termine. En consecuencia, para probar la corrección total de un programa, basta con probar su corrección parcial y su terminación. ^{[ 2 ]} Este último tipo de prueba ( prueba de terminación ) nunca puede automatizarse por completo, ya que el problema de la parada es indecidible .

Por ejemplo, buscar sucesivamente en los enteros positivos (1, 2, 3, …) para ver si podemos encontrar un número perfecto impar es bastante fácil de escribir y es un programa parcialmente correcto que encontraría un número perfecto impar, si tal número existe (véase el recuadro). Sin embargo, afirmar que este programa es totalmente correcto (es decir, que encontrará dicho número y terminará) sería afirmar que un número perfecto impar realmente existe, lo cual actualmente se desconoce en la teoría de números .

La demostración tendría que ser 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 las limitaciones de la memoria de la computadora .

Un resultado fundamental en la teoría de la demostración , la correspondencia de Curry-Howard , establece que una demostración de corrección funcional en lógica constructiva se corresponde con un programa determinado en el cálculo lambda . Convertir una demostración de esta manera se denomina extracción de programas .

La lógica de Hoare es un sistema formal específico para razonar rigurosamente sobre la corrección de los programas informáticos. ^{[ 3 ]} Utiliza técnicas axiomáticas para definir la semántica de los lenguajes de programación y argumentar sobre la corrección de los programas mediante aserciones 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 que cumple con los resultados requeridos. Si bien son cruciales para la calidad del software y ampliamente utilizadas por programadores y evaluadores, las pruebas de software aún se consideran un arte debido a la comprensión limitada de los principios del software. La dificultad de las pruebas de software radica en la complejidad del software: no podemos probar completamente un programa de complejidad moderada. Las pruebas van más allá de la simple depuración. Su propósito puede ser el aseguramiento de la calidad, la verificación y validación, o la estimación de la confiabilidad. También pueden utilizarse como una 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 implican un equilibrio entre presupuesto, tiempo y calidad. ^{[ 4 ]}

• Verificación formal
• Diseño por contrato
• Análisis del programa
• Verificación de modelos
• Corrección del compilador
• Derivación del programa

• « Tecnología del lenguaje humano. Desafíos para la informática y la lingüística ». Google Books. Sin paginar, sin fecha. Web. 10 de abril de 2017.
• " Seguridad en la informática y las comunicaciones ". Google Books. Sin paginar, sin fecha. Web. 10 de abril de 2017.
• « El problema de la parada de Alan Turing: una explicación muy amena e ilustrada ». El problema de la parada de Alan Turing: una explicación muy amena e ilustrada. Sin lugar de publicación. 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 de programas". Universidad de Texas en Austin, Departamentos de Matemáticas y Ciencias de la Computación, Proyecto de Demostración Automática de Teoremas, 1970. Web.