Corrección (informática)
Calidad de un algoritmo que es correcto con respecto a una especificación

En informática teórica , un algoritmo es correcto con respecto a una especificación si se comporta como se especifica. Lo mejor es explorar 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 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, que el algoritmo finalice. 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 finalización ) nunca puede automatizarse por completo, ya que el problema de detención es indecidible .

Programa en C parcialmente correcto para encontrar
el número perfecto menos impar,
su exactitud total se desconoce a partir de 2023
// devuelve la suma de los divisores propios de n static int divisorSum ( int n ) { int i , suma = 0 ; for ( i = 1 ; i < n ; ++ i ) if ( n % i == 0 ) suma += i ; return suma ; } // devuelve el número perfecto menos impar int lessPerfectNumber ( void ) { int n ; for ( n = 1 ; ; n += 2 ) if ( n == divisorSum ( n )) return n ; }

Por ejemplo, si buscamos 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 (véase el recuadro). Pero decir que este programa es totalmente correcto sería afirmar algo que actualmente no se sabe 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 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 dada. Eso implicaría consideraciones tales como limitaciones en la memoria de la computadora .

Un resultado profundo de la teoría de pruebas , la correspondencia Curry-Howard , establece que una prueba de corrección funcional en lógica constructiva corresponde a un programa determinado en el cálculo lambda . La conversión de una prueba de esta manera 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 informáticos. [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 utilizadas 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 surge de la complejidad del software: no podemos probar completamente un programa con una complejidad moderada. Las pruebas son más que una simple depuración. 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 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 son un equilibrio entre presupuesto, tiempo y calidad. [4]

Véase también

Notas

  1. ^ Dunlop, Douglas D.; Basili, Victor R. (junio de 1982). "Un análisis comparativo de la corrección funcional". Comunicaciones de la ACM . 14 (2): 229–244. doi :10.1145/356876.356881. S2CID  18627112.
  2. ^ Manna, Zohar; Pnueli, Amir (septiembre de 1974). "Enfoque axiomático para la corrección total de los programas". Acta Informatica . 3 (3): 243–263. doi :10.1007/BF00288637. S2CID  2988073.
  3. ^ 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. S2CID  207726175. Archivado desde el original (PDF) el 4 de marzo de 2016. 
  4. ^ Pan, Jiantao (primavera de 1999). "Software Testing" (trabajo de curso). Carnegie Mellon University . Consultado el 21 de noviembre de 2017 .

Referencias

  • "Tecnología del lenguaje humano. Desafíos para la informática y la lingüística". Google Books. Sin fecha, sin fecha. Web. 10 de abril de 2017.
  • "Seguridad en la informática y las comunicaciones". Google Books. Np, nd Web. 10 de abril de 2017.
  • "El problema de la detención de Alan Turing: una explicación muy alegre e ilustrada". The Halting Problem of Alan Turing - A Most Merry and Illustrated Explanation. Np, nd Web. 10 de abril de 2017.
  • Turner, Raymond y Nicola Angius. "La filosofía de la informática". Stanford Encyclopedia of Philosophy . Stanford University, 20 de agosto de 2013. Web. 10 de abril de 2017.
  • Dijkstra, EW "Program Correctness". 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.
Obtenido de "https://es.wikipedia.org/w/index.php?title=Corrección_(informática)&oldid=1229003987"