¿Las pruebas de corrección de código alguna vez se generalizarán? [cerrado]

14

Todos los programas, excepto los más triviales, están llenos de errores, por lo que todo lo que prometa eliminarlos es extremadamente atractivo. En este momento, las pruebas de corrección son un código extremadamente esotérico, principalmente debido a la dificultad de aprender esto y al esfuerzo adicional que se necesita para probar que un programa es correcto. ¿Crees que el código de prueba despegará?

    
pregunta Casebash 02.09.2010 - 23:54
fuente

10 respuestas

8

No realmente en ese sentido, pero la programación funcional pura es buena en este dominio. Si usas Haskell, es probable que tu programa sea correcto si el código se compila. Excepto de IO, un buen sistema de tipos es una buena ayuda.

También la programación para contratar puede ser útil. Consulte Contratos de código de Microsoft

    
respondido por el Jonas 03.09.2010 - 00:49
fuente
14
  

Todos los programas menos triviales

no se puede probar completamente para que sea correcto con un esfuerzo razonable. Para cualquier prueba formal de corrección, necesita al menos una especificación formal, y esa especificación debe estar completa y correcta. Esto normalmente no es nada que pueda crear fácilmente para la mayoría de los programas del mundo real. Por ejemplo, intente escribir una especificación de este tipo para algo como la interfaz de usuario de este sitio de discusión, y sabrá a qué me refiero.

Aquí encontré un buen artículo sobre el tema:

enlace

    
respondido por el Doc Brown 22.12.2011 - 16:06
fuente
10

El problema con las pruebas formales es que solo hace que el problema retroceda un paso.

Decir que un programa es correcto equivale a decir que un programa hace lo que debe hacer. ¿Cómo se define lo que debe hacer el programa? Usted lo especifica. ¿Y cómo define lo que debe hacer el programa en los casos perimetrales que la especificación no cubre? Bueno, entonces tienes que hacer las especificaciones más detalladas.

Entonces, digamos que su especificación finalmente se vuelve lo suficientemente detallada para describir el comportamiento correcto de cada aspecto del programa completo. Ahora necesitas una manera de hacer que tus herramientas de prueba lo entiendan. Entonces, tiene que traducir la especificación a algún tipo de lenguaje formal que la herramienta de prueba pueda entender ... hey, ¡espere un minuto!

    
respondido por el Mason Wheeler 22.12.2011 - 18:52
fuente
8

La verificación formal ha recorrido un largo camino, pero por lo general, las herramientas ampliamente utilizadas por la industria están a la zaga de las últimas investigaciones. Aquí hay algunos esfuerzos recientes en esta dirección:

Spec # enlace Esta es una extensión de C # que admite contratos de código (condiciones pre / post e invariantes) y puede usar estos contratos para realizar varios tipos de análisis estático.

Existen proyectos similares a este para otros idiomas, como JML para java, y Eiffel tiene esto prácticamente incorporado.

Yendo aún más lejos, proyectos como slam y blast se puede usar para verificar ciertas propiedades de comportamiento con una mínima anotación / intervención del programador, pero aún no puede manejar la generalidad completa de los lenguajes modernos ( cosas como el desbordamiento de enteros / aritmética de punteros no están modeladas).

Creo que veremos muchas más de estas técnicas utilizadas en la práctica en el futuro. La principal barrera es que los invariantes del programa son difíciles de inferir sin anotaciones manuales, y los programadores generalmente no están dispuestos a proporcionar estas anotaciones porque hacerlo es demasiado tedioso / lento.

    
respondido por el Lucina 22.12.2011 - 15:49
fuente
4

No a menos que surja un método para probar automáticamente el código sin un extenso trabajo de desarrollador.

    
respondido por el Fishtoaster 03.09.2010 - 00:35
fuente
3

Algunas herramientas métodos formales (como por ejemplo Frama-C para el software C incorporado crítico) se puede ver como (una especie de) proporcionando, o al menos comprobando, una prueba (correcta) de un software determinado. (Frama-C verifica que un programa obedezca a su especificación formalizada, en cierto sentido, y respete las invariantes anotadas explícitamente en el programa).

En algunos sectores, tales métodos formales son posibles, por ejemplo, como DO-178C para software crítico en aviones civiles. Entonces, en algunos casos, tales enfoques son posibles y útiles.

Por supuesto, el desarrollo de software con menos errores es muy costoso. Pero el enfoque del método formal tiene sentido para algún tipo de software. Si es pesimista, podría pensar que el error se mueve del código a su especificación formal (que puede tener algunos "errores", porque formalizar el comportamiento previsto de un software es difícil y propenso a errores).

    
respondido por el Basile Starynkevitch 22.12.2011 - 16:34
fuente
3

Me topé con esta pregunta y creo que este enlace podría ser interesante:

Aplicaciones industriales de Astrée

Probar la ausencia de RTE en un sistema utilizado por Airbus con más de 130K líneas de código en 2003 no parece ser malo, y me pregunto si habrá alguien que diga que esto no es un mundo real.

    
respondido por el Ziyao Wei 11.02.2012 - 02:31
fuente
2

No. El proverbio común para esto es: "En teoría, la teoría y la práctica son lo mismo. En la práctica, no".

Un ejemplo muy simple: Typos.

En realidad, ejecutar el código a través de pruebas unitarias encuentra estas cosas casi de inmediato, y un conjunto cohesivo de pruebas anulará la necesidad de cualquier prueba formal. Todos los casos de uso (bueno, malo, error y borde) se deben enumerar en las pruebas unitarias, que terminan como una mejor prueba de que el código es correcto que cualquier otra prueba separada del código.

Especialmente si los requisitos cambian o el algoritmo se actualiza para corregir un error: es más probable que la prueba formal quede desactualizada, al igual que los comentarios de código a menudo.

    
respondido por el Izkata 22.12.2011 - 17:06
fuente
1

Creo que los límites impuestos en las pruebas de corrección debido al problema de detención pueden ser la barrera más grande para que se conviertan mainstream.

    
respondido por el Paddyslacker 03.09.2010 - 00:40
fuente
1

Ya es usado por todos. Cada vez que utiliza la verificación de tipos de su lenguaje de programación, básicamente está haciendo una prueba matemática de la corrección de su programa. Esto ya funciona muy bien, solo requiere que elijas los tipos correctos para cada función y estructura de datos que uses. Cuanto más preciso sea el tipo, mejor será la comprobación que obtendrá. Los tipos existentes disponibles en lenguajes de programación ya tienen herramientas suficientemente poderosas para describir casi cualquier comportamiento posible. Esto funciona en todos los idiomas disponibles. C ++ y los lenguajes estáticos solo hacen las comprobaciones en tiempo de compilación, mientras que los lenguajes más dinámicos como python lo hacen cuando se ejecuta el programa. El cheque todavía existe en todos estos idiomas. (por ejemplo, c ++ ya admite la comprobación de efectos secundarios de la misma manera que lo hace haskell, pero solo tiene que elegir usarlo).

    
respondido por el tp1 22.12.2011 - 18:34
fuente

Lea otras preguntas en las etiquetas