¿Hay alguna teoría formal / matemática de las pruebas de software?

Buscar en Google "teoría de prueba de software" solo parece dar teorías en el sentido blando de la palabra; No he podido encontrar nada que clasifique como teoría en el sentido matemático, teórico de la información o en algún otro campo científico.

Lo que estoy buscando es algo que formalice qué es la prueba, las nociones utilizadas, qué es un caso de prueba, la viabilidad de probar algo, la practicidad de probar algo, la medida en que algo debe probarse, la definición / explicación formal de cobertura de código, etc.

ACTUALIZACIÓN: Además, no estoy seguro, intuitivamente, sobre la conexión entre la verificación formal y lo que pregunté, pero claramente hay algún tipo de conexión.

Para un libro que explora las matemáticas detrás de las pruebas de software ... el libro fundamental para obtener es El arte del análisis de rendimiento de los sistemas informáticos: técnicas para diseño experimental, medición, simulación y modelado

Si bien se publicó por primera vez en 1991, sigue siendo popular hoy en día porque es un libro de matemáticas aplicadas que se centra únicamente en el análisis de rendimiento, la simulación y las mediciones.

No puedo señalar un buen recurso en línea (los artículos de Wikipedia en inglés sobre estos temas tienden a ser mejorables), pero puedo resumir una conferencia que escuché que también cubría la teoría básica de las pruebas.

Modos de prueba

Existen diferentes clases de pruebas, como pruebas unitarias o pruebas de integración . Una prueba unitaria afirma que una pieza de código coherente (función, clase, módulo) tomada en sus propios trabajos como se esperaba, mientras que una prueba de integración afirma que varias de esas piezas funcionan correctamente juntas.

Un caso de prueba es un entorno conocido en el que se ejecuta un fragmento de código, por ejemplo, utilizando una entrada de prueba específica o burlándose de otras clases. El comportamiento del código se compara con el comportamiento esperado, por ejemplo, un valor de retorno específico.

Una prueba solo puede probar la presencia de un error, nunca la ausencia de todos los errores. Las pruebas ponen un límite superior a la corrección del programa.

Cobertura de código

Para definir métricas de cobertura de código, el código fuente se puede traducir a un gráfico de flujo de control donde cada nodo contiene un segmento lineal del código. El control fluye entre estos nodos solo al final de cada bloque, y siempre es condicional (si es condición, entonces goto node A, de lo contrario goto node B). El gráfico tiene un nodo inicial y un nodo final.

• Con este gráfico, la cobertura de la declaración es la relación de todos los nodos visitados a todos los nodos. La cobertura completa del estado de cuenta no es suficiente para realizar pruebas exhaustivas.
• La cobertura de rama es la relación de todos los bordes visitados entre nodos en el CFG y todos los bordes. Esto prueba insuficientemente los bucles.
• La cobertura de ruta es la proporción de todas las rutas visitadas a todas las rutas, donde una ruta es cualquier secuencia de bordes desde el nodo inicial hasta el final. El problema es que con los bucles, puede haber un número infinito de rutas, por lo que la cobertura de ruta completa no se puede probar prácticamente.

Por lo tanto, a menudo es útil verificar la cobertura de la condición .

• En una cobertura de condición simple , cada condición atómica es una vez verdadera y una vez falsa, pero esto no garantiza la cobertura completa de la declaración.
• En la cobertura de múltiples condiciones , las condiciones atómicas han adquirido todas las combinaciones de truey false. Esto implica una cobertura de sucursal completa, pero es bastante costoso. El programa puede tener restricciones adicionales que excluyen ciertas combinaciones. Esta técnica es buena para obtener cobertura de sucursal, puede encontrar código muerto, pero no puede encontrar errores derivados de la condición incorrecta .
• En la cobertura de condición múltiple mínima , cada condición atómica y compuesta es una vez verdadera y falsa. Todavía implica una cobertura total de la sucursal. Es un subconjunto de cobertura de múltiples afecciones, pero requiere menos casos de prueba.

Al construir una entrada de prueba utilizando la cobertura de la condición, se debe tener en cuenta el cortocircuito. Por ejemplo,

function foo(A, B) {
  if (A && B) x()
  else        y()
}

debe probarse con foo(false, whatever), foo(true, false)y foo(true, true)para una cobertura mínima mínima de múltiples condiciones.

Si tiene objetos que pueden estar en múltiples estados, entonces probar todas las transiciones de estado análogas a los flujos de control parece razonable.

Hay algunas métricas de cobertura más complejas, pero generalmente son similares a las métricas presentadas aquí.

Estos son métodos de prueba de caja blanca y pueden ser parcialmente automatizados. Tenga en cuenta que un conjunto de pruebas unitarias debe tener como objetivo tener una alta cobertura de código por cualquier métrica elegida, pero el 100% no siempre es posible. Es especialmente difícil probar el manejo de excepciones, donde las fallas deben inyectarse en ubicaciones específicas.

Pruebas funcionales

Luego hay pruebas funcionales que afirman que el código se adhiere a la especificación al ver la implementación como un cuadro negro. Tales pruebas son útiles para pruebas unitarias y pruebas de integración por igual. Debido a que es imposible probar con todos los datos de entrada posibles (por ejemplo, probar la longitud de la cadena con todas las cadenas posibles), es útil agrupar la entrada (y la salida) en clases equivalentes; si length("foo")es correcto, foo("bar")es probable que también funcione. Para cada combinación posible entre las clases de equivalencia de entrada y salida, se elige y prueba al menos una entrada representativa.

Uno debe probar adicionalmente

• casos extremos length(""), foo("x"), length(longer_than_INT_MAX),
• valores permitidos por el lenguaje, pero no por el contrato de la función length(null), y
• posibles datos basura length("null byte in \x00 the middle")...

Con números, esto significa probar 0, ±1, ±x, MAX, MIN, ±∞, NaN, y con comparaciones de punto flotante probar dos flotadores vecinos. Como otra adición, se pueden elegir valores de prueba aleatorios de las clases de equivalencia. Para facilitar la depuración, vale la pena registrar la semilla utilizada ...

Pruebas no funcionales: pruebas de carga, pruebas de estrés

Una pieza de software tiene requisitos no funcionales, que también deben ser probados. Estos incluyen pruebas en los límites definidos (pruebas de carga) y más allá de ellos (pruebas de esfuerzo). Para un juego de computadora, esto podría ser afirmar un número mínimo de fotogramas por segundo en una prueba de carga. Un sitio web puede ser sometido a pruebas de estrés para observar los tiempos de respuesta cuando el doble de visitantes que los anticipados están maltratando los servidores. Tales pruebas no solo son relevantes para sistemas completos sino también para entidades individuales: ¿cómo se degrada una tabla hash con un millón de entradas?

Otros tipos de pruebas son pruebas de todo el sistema en las que se simulan escenarios o pruebas de aceptación para demostrar que se cumplió el contrato de desarrollo.

Métodos sin prueba

Comentarios

Existen técnicas que no son de prueba que se pueden usar para garantizar la calidad. Los ejemplos son tutoriales, revisiones formales de código o programación de pares. Si bien algunas partes se pueden automatizar (por ejemplo, utilizando linters), generalmente requieren mucho tiempo. Sin embargo, las revisiones de código por parte de programadores experimentados tienen una alta tasa de descubrimiento de errores y son especialmente valiosas durante el diseño, donde no es posible realizar pruebas automatizadas.

Cuando las revisiones de código son tan buenas, ¿por qué seguimos escribiendo pruebas? La gran ventaja de los conjuntos de pruebas es que pueden ejecutarse (en su mayoría) automáticamente y, como tales, son muy útiles para las pruebas de regresión .

Verificación formal

La verificación formal va y prueba ciertas propiedades del código. La verificación manual es principalmente viable para partes críticas, menos para programas completos. Las pruebas ponen un límite inferior a la corrección del programa. Las pruebas se pueden automatizar hasta cierto punto, por ejemplo, a través de un verificador de tipo estático.

Ciertas invariantes se pueden verificar explícitamente mediante el uso de assertdeclaraciones.

Todas estas técnicas tienen su lugar y son complementarias. TDD escribe las pruebas funcionales por adelantado, pero las pruebas pueden juzgarse por sus métricas de cobertura una vez que se implementa el código.

Escribir código comprobable significa escribir pequeñas unidades de código que se pueden probar por separado (funciones auxiliares con granularidad adecuada, principio de responsabilidad única). Cuantos menos argumentos tome cada función, mejor. Dicho código también se presta para la inserción de objetos simulados, por ejemplo, mediante inyección de dependencia.

Quizás las "pruebas basadas en especificaciones" también respondan a su pregunta. Verifique estos módulos de prueba (que aún no he usado). Requieren que escriba una expresión matemática para especificar conjuntos de valores de prueba, en lugar de escribir una prueba unitaria utilizando valores de datos individuales seleccionados.

Prueba :: Lectrotest

Como dice el autor, este módulo Perl se inspiró en el módulo Quick-Check de Haskell . Hay más enlaces en esta página, algunos de los cuales están muertos.

Un enfoque matemático es la prueba de todas las parejas . La idea es que la mayoría de los errores se activan mediante una única opción de configuración, y la mayoría del resto se activa mediante un cierto par de opciones tomadas simultáneamente. Así, la mayoría puede ser atrapado probando "todos los pares". Una explicación matemática (con generalizaciones) está aquí:

El sistema AETG: un enfoque para las pruebas basado en el diseño combinatorio

(hay muchas más referencias de este tipo)

Se utilizan algunas ecuaciones matemáticas, pero depende del tipo de prueba de software que esté utilizando. Por ejemplo, la suposición de falla crítica supone que las fallas no son producto de 2 o más fallas simultáneas. La siguiente ecuación es: f = 4n + 1. f = la función que calcula el número de casos de prueba para un número dado de variables ( n) + 1 es la suma de la constante donde todas las variables asumen el valor nominal.

Otro tipo de prueba que requiere ecuaciones matemáticas es la prueba de robustez que prueba la solidez o la corrección de los casos de prueba en un proceso de prueba. En esta prueba, ingresaría variables dentro del rango de entrada legítimo (casos de prueba limpios) y variables de entrada fuera del rango de entrada (casos de prueba sucios). Usaría la siguiente ecuación matemática: f = 6n + 1 . 6n indica que cada variable tiene que asumir 6 valores diferentes mientras que los otros valores asumen el valor nominal. * + 1 * representa la suma de la constante 1.