¿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 promete eliminarlos es extremadamente atractivo. Por el momento, las pruebas de corrección son código es extremadamente esotérico, principalmente debido a la dificultad de aprender esto y el esfuerzo adicional que se requiere para probar que un programa es correcto. ¿Crees que la prueba de código despegará?

programming-practices Casebash
fuente

Respuestas:

8

No realmente 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 programar para contratar puede ser útil. Ver contratos de código de Microsoft

Jonas
fuente
66
Lo siento, no he hecho mucho Haskell del "mundo real", pero he hecho suficientes ejercicios de tutoría para varias vidas. Solo porque se compila no significa que sea probable que funcione. En comparación con, por ejemplo, Ada (elegido porque es un lenguaje imperativo estrictamente tipado estáticamente), diría que Haskell es un poco más fácil, pero principalmente porque es más conciso (menor complejidad ciclomática). Cuando se trata de la mónada IO, hay molestias que pueden hacer que Haskell sea más difícil de corregir: es lo suficientemente diferente del estilo imperativo que hay cosas que no puede hacer de forma natural.
Steve314
En "no se puede hacer tan naturalmente", considere un bucle "while". Sí, puede rodar el suyo, pero la condición while debe estar dentro de la mónada porque necesita reaccionar a los efectos secundarios del cuerpo del bucle. Esto no solo significa que se le ha dado permiso para causar efectos secundarios dentro de la condición while, sino que también hace que sea difícil usar ese ciclo while. Resultado final: generalmente es más fácil usar la recursividad incluso en el código IO monad, y eso significa que tiene que estructurar las cosas de una manera particular.
Steve314
14

Todos menos los programas más triviales

no se puede probar 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. Normalmente, esto no es nada que pueda crear fácilmente para la mayoría de los programas del mundo real. Por ejemplo, intente escribir tal especificación 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-procorcornessnessproof.html

Doc Brown
fuente
Correcto: para cualquier proyecto de programación hay una transición de una descripción informal del problema a una formal (generalmente, hoy, en forma de un programa), y eso no va a desaparecer.
David Thornley
astree.ens.fr Ver aplicaciones industriales de Astrée aquí
zw324
@ ZiyaoWei: tales herramientas son útiles, pero solo encuentran algunos errores formales, no más. Si un programa de una línea como printf("1")es correcto o no (por ejemplo, porque el requisito era "imprimir un número aleatorio igualmente distribuido de 1 a 6") no puede decidirse con un analizador estático de este tipo.
Doc Brown
10

El problema con las pruebas formales es que solo mueve el problema un paso atrás.

Decir que un programa es correcto es equivalente a decir que un programa hace lo que debería hacer. ¿Cómo define lo que debe hacer el programa? Usted lo especifica ¿Y cómo define lo que debe hacer el programa en casos extremos 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 manera 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!

Mason Wheeler
fuente
2
Además ... "Tenga cuidado con los errores en el código anterior; solo he demostrado que es correcto, no lo he probado". - Donald Knuth
Brendan
8

La verificación formal ha recorrido un largo camino, pero generalmente las herramientas de la industria / ampliamente utilizadas van a la zaga 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 idiomas, como JML para Java, y Eiffel tiene esto bastante integrado.

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

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

Lucina
fuente
4

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

Fishtoaster
fuente
Considere el argumento económico: tal vez sea mejor para los desarrolladores "perder" el tiempo con pruebas de corrección que perder dinero debido a errores de software.
Andres F.
Estoy de acuerdo con fishtoaster, a menos que sea mucho menos intensivo en recursos, una gran cantidad de software comercial regular simplemente no tendrá el costo / beneficio para soportar ese nivel de corrección. En una aplicación LOB para una audiencia cautiva, a veces el mayor beneficio comercial por el costo con respecto a un informe de error es agregar una línea a los documentos que dice "no hagas eso"
Bill
3

Algunas herramientas de métodos formales (como, por ejemplo, Frama-C para software C incrustado crítico) se pueden ver como (una especie de) que proporcionan, o al menos comprueban, una prueba (correcta) de un software dado. (Frama-C verifica que un programa obedezca su especificación formalizada, en cierto sentido, y respete invariablemente las anotaciones anotadas en el programa).

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

Por supuesto, desarrollar 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, puede 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).

Basile Starynkevitch
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 130,000 líneas de código en 2003 no parece ser malo, y me pregunto si habrá alguien que diga que este no es el mundo real.

zw324
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: 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 negará la necesidad de pruebas formales. Todos los casos de uso (buenos, malos, errores y casos extremos) 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 los requisitos cambian o 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.

Izkata
fuente
3
Incorrecto. Ninguna prueba unitaria podrá cubrir todo el rango de parámetros posibles. Imagine "pruebas unitarias" de un compilador de esta manera, asegurándose de que no pase semántica de cambio.
SK-logic
3
las pruebas unitarias no son el santo grial ...
Ryathal
1
@ Winston Ewert, hay compiladores verificados (y muchos más ensambladores verificados). Y el hardware se verifica formalmente con mucha más frecuencia que el software. Ver aquí: gallium.inria.fr/~xleroy/publi/compiler-certif.pdf
SK-logic
1
@ SK-logic, sí, hay compiladores de juguetes que han demostrado ser correctos para fines académicos. ¿Pero qué pasa con los compiladores que la gente realmente usa? Sospecho que la mayoría de los compiladores se verifican mediante diversas formas de pruebas automatizadas y casi no se realizan pruebas formales correctas.
Winston Ewert
1
@ Winston Ewert, las pruebas de corrección son prácticas y se utilizan ampliamente en la vida real. Lo que no es muy práctico es la mayoría de los idiomas principales modernos. Espero que todos desaparezcan, por lo que el valor de las pruebas de corrección aumentará en el futuro.
SK-logic
1

Creo que los límites impuestos a las pruebas de corrección debido al problema de detención podrían ser la mayor barrera para que las pruebas de corrección se generalicen.

Paddyslacker
fuente
8
El problema de detención dice que no podemos determinar si algún programa arbitrario se detiene. Estos programas pueden hacer cosas raras, como probar cada número entero para ver si es un Mersenne prime. ¡No hacemos esto en programas normales!
Casebash
1
@Casebash, la pregunta es si existe un subconjunto útil de programas para el cual se pueda resolver el problema de detención. Eso de ninguna manera está claro de ninguna manera. Es decir, ¿podemos restringir nuestros programas para que no podamos hacer cosas como probar cada número entero sin arruinar nuestra capacidad de realizar tareas útiles?
Winston Ewert
1

Ya lo usan todos. Cada vez que utiliza la verificación de tipo de su lenguaje de programación, básicamente está haciendo una prueba matemática de la exactitud de su programa. Esto ya funciona muy bien, solo requiere que elija los tipos correctos para cada función y estructura de datos que utiliza. 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 lo suficientemente potentes como para describir casi cualquier comportamiento posible. Esto funciona en todos los idiomas disponibles. C ++ y los lenguajes estáticos solo están haciendo 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,

tp1
fuente
Con un poco sobre los efectos secundarios en C ++, ¿te refieres a la corrección constante?
Winston Ewert
sí, const + const función miembro. Si todas sus funciones miembro son constantes, todos los datos en los objetos no se pueden modificar.
tp1
Todavía son modificables si usa mutableo const_cast. Ciertamente veo la conexión que trazas allí, pero el sabor de dos enfoques me parece bastante diferente.
Winston Ewert
Bueno, es por eso que debes elegir usarlo: siempre hay formas de evitarlo. Pero lo importante es cómo hacer que los compiladores verifiquen si hay problemas en el área.
tp1