it-swarm-es.com

¿Se generalizarán alguna vez las pruebas de corrección del código?

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

14
Casebash

Realmente no en ese sentido, pero la programación funcional pura es buena en este dominio. Si usa Haskell, es probable que su programa sea correcto si el código se compila. Excepto por 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

8
Jonas

Todos menos los programas más triviales

no se puede probar completamente 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 ser completa y correcta. Por lo general, esto 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 ya sabe a qué me refiero.

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

http://www.encyclopedia.com/doc/1O11-programcorrectnessproof.html

14
Doc Brown

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

Decir que un programa es correcto equivale a decir que un programa hace lo que debería hacer. ¿Cómo define lo que debe hacer el programa? Tú lo especificas. ¿Y cómo se define lo que debe hacer el programa en los casos de Edge que la especificación no cubre? Bueno, entonces tienes que hacer la especificación más detallada.

Entonces, digamos que su especificación finalmente se vuelve lo suficientemente detallada como para describir el comportamiento correcto de cada aspecto de todo el programa. Ahora necesita una forma de hacer que sus herramientas de prueba lo entiendan. Así que tienes que traducir la especificación a algún tipo de lenguaje formal que la herramienta de prueba pueda entender ... ¡oye, espera un minuto!

10
Mason Wheeler

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

Spec # http://research.Microsoft.com/en-us/projects/specsharp/ Esta es una extensión de C # que admite contratos de código (condiciones previas/posteriores e invariantes) y puede usar estos contratos para hacer varios tipos de análisis estático.

Existen proyectos similares a este para otros lenguajes, como JML para Java, y Eiffel tiene esto prácticamente integrado.

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

Creo que veremos muchas más de estas técnicas utilizadas en la práctica en el futuro. La principal barrera es que las 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/consume mucho tiempo.

8
Lucina

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

4
Fishtoaster

Me encontré 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 estar mal, y me pregunto si alguien dirá que este no es el mundo real.

3
zw324

Algunas métodos formales herramientas (como, por ejemplo, Frama-C para software C incrustado crítico) pueden verse como (más o menos) que proporcionan, o al menos verifican, una (corrección) prueba de un software determinado. (Frama-C comprueba que un programa obedece a su especificación formalizada, en cierto sentido, y respeta las invariantes anotadas explícitamente en el programa).

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

Por supuesto, desarrollar un 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 ha trasladado 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).

3

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: errores tipográficos.

En realidad, ejecutar el código a través de pruebas unitarias encuentra tales cosas casi de inmediato, y un conjunto coherente de pruebas anulará la necesidad de pruebas formales. Todos los casos de uso (buenos, malos, errores y casos Edge) deben enumerarse en las pruebas unitarias, que terminan como una mejor prueba de que el código es correcto que cualquier prueba que esté separada del código.

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

2
Izkata

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

1
Paddyslacker

Ya lo usan todos. Cada vez que usa 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 elija los tipos correctos para cada función y estructura de datos que use. Cuanto más preciso sea el tipo, mejor comprobación obtendrá. Los tipos existentes disponibles en los lenguajes de programación ya tienen herramientas lo suficientemente potentes como 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 lenguajes más dinámicos como python lo hacen cuando se ejecuta el programa. La comprobación todavía existe en todos estos lenguajes. (Por Por ejemplo, c ++ ya admite la verificación de efectos secundarios de la misma manera que lo hace Haskell, pero solo necesita elegir usarlo).

1
tp1