¿Es la "prueba de unidad" una forma de método formal?

7

Después de algunas investigaciones, entiendo que:

Como veo aquí , una prueba formal es solo un cálculo matemático, basado en una expresión matemática (expresión booleana).

Se comprueba una prueba de unidad a partir de aserciones, así que principalmente en una o en un conjunto de expresiones booleanas.

Además, leí (muy rápidamente) un documento de investigación sobre la generación de pruebas unitarias de prueba formal.

  • ¿La prueba de unidad es una forma de método formal (aquí creo que para un sistema como prueba formal)?
  • Si es un concepto totalmente separado, ¿cuáles son las diferencias?

El objetivo de esta pregunta es no saber si después de ejecutar la prueba de la unidad todavía hay errores. Su objetivo es saber si existe un vínculo entre las pruebas unitarias y el método formal.

    
pregunta csblo 10.04.2015 - 10:28

2 respuestas

25

Las dos cosas son diferentes y, de hecho, son mucho más diferentes en la práctica de lo que serían en teoría.

Una prueba de corrección formal demuestra algo sobre el comportamiento de un algoritmo . Por ejemplo, podría investigar los invariantes que se aplican a los datos a medida que se transforma mediante un algoritmo de clasificación, y probar que si el algoritmo termina, cada elemento es más grande que el anterior. Este tipo de prueba puede ser rigurosa, es decir, si se realiza correctamente, el algoritmo no puede estar equivocado a este respecto.

En la práctica, los algoritmos deben estar incorporados en un código de computadora, y generalmente no es factible probar que un bit dado de código representa con precisión el algoritmo que desea. (Eso requeriría probar formalmente el comportamiento del compilador, la biblioteca estándar, la máquina virtual, etc.) Se vuelve un poco más fácil cuanto más similar es el lenguaje de programación a la notación matemática que ha usado en la prueba formal, pero no mucho. (Se dijo que el código que se ejecuta en los sistemas centrales del Transbordador espacial es casi una notación matemática perfecta en sí mismo, pero no es muy agradable de programar).

Es mucho más rentable ejecutar el código en entradas cuidadosamente seleccionadas y verificar que produzca las salidas esperadas. Esto tiene la desventaja de que nunca se puede estar seguro de que no haya un error, podría comportarse para los pares de entrada / salida que no haya probado (y generalmente hay más pares de los que puede probar, o no lo haría). t necesita un programa de computadora para hacer el trabajo en primer lugar, o peor, el código puede ser sutilmente no determinista o dependiente del contexto de manera que sus pruebas no se expongan.

Pero en la práctica, la mayoría de los errores que afectan a una computación puede exponerse con verificaciones inteligentes, y si mantiene un registro de errores conocidos y casos de prueba que verifican que no pueden repetirse , la calidad del código generalmente puede ser lo suficientemente buena como para tener un valor comercial. Ciertamente, es una mejor idea realizar pruebas unitarias, pruebas de integración y pruebas de aceptación del usuario y sacar algo por la puerta que la gente pagará en lugar de realizar una prueba formal larga y costosa que pasa por alto una desviación sutil entre la especificación escrita y el las expectativas actuales del cliente. Así que en el mundo real, las dos son actividades casi completamente distintas.

    
respondido por el Kilian Foth 10.04.2015 - 10:43
9

No existe una definición precisa y universalmente aceptada de "método formal". Sin embargo, la mayoría de las definiciones implican alguna forma de rigor matemático, formalismo o prueba, ninguna de las cuales proporciona una prueba de unidad.

Una prueba de unidad es simplemente "pruébelo y vea si funciona en este único caso específico", mientras que los métodos formales intentan demostrar que "siempre funciona en todos los casos en todas las condiciones en todos los entornos".

    
respondido por el Jörg W Mittag 10.04.2015 - 11:21

Lea otras preguntas en las etiquetas

Comentarios Recientes

O hablando formalmente: ¿un método formal con el que desarrollaste la prueba? Reconozco que los métodos formales se consideran fantásticos, emocionantes y definitivamente le dirían a uno de mis al menos nueve graduados de Harvard lo increíble que me he convertido como programador en los últimos nueve años. Supongo que por eso me gustan los hechos. Pero en la comunidad de programación "hostil". Lo que siempre he dudado de hacer es ser amigable con la multitud anti formal. Entonces, esta publicación de blog... Lee mas