Corrección (ciencias de la computación) - Correctness (computer science)

En informática teórica , un algoritmo es correcto con respecto a una especificación si se comporta como se especifica. Lo mejor que se explora 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).

Dentro de la última noción, corrección parcial , requiriendo que si una respuesta es devuelta será correcta, se distingue de la corrección total de , que, además, requiere que una respuesta se regresó el tiempo, 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 terminación. El último tipo de prueba (prueba de terminación ) nunca puede automatizarse por completo, ya que el problema de la detención es indecidible .

Programa C parcialmente correcto para encontrar
el número perfecto menos impar,
se desconoce su exactitud total a partir de 2021 
// return the sum of proper divisors of n
static int divisorSum(int n) {
   int i, sum = 0;
   for (i=1; i<n; ++i)
      if (n % i == 0)
         sum += i;
   return sum;
}
// return the least odd perfect number
int leastPerfectNumber(void) {
   int n;
   for (n=1; ; n+=2)
      if (n == divisorSum(n))
         return n;
}

Por ejemplo, buscando sucesivamente entre los números 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 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 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. 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.

Ver también

Notas

Referencias