¿Por qué no se pueden probar los programas?

https://stackoverflow.com/questions/476959

20-08-2019
|

Pregunta

¿Por qué no se puede demostrar un programa de computadora del mismo modo que se puede probar un enunciado matemático?Una prueba matemática se construye sobre otras pruebas, que a su vez se construyen a partir de más pruebas y hasta llegar a los axiomas: aquellas verdades que consideramos evidentes por sí mismas.

Los programas informáticos no parecen tener esa estructura.Si escribes un programa de computadora, ¿cómo es posible que puedas tomar trabajos previos probados y usarlos para mostrar la verdad de tu programa?No puedes porque no existe ninguno.Además, ¿cuáles son los axiomas de la programación?¿Las verdades muy atómicas del campo?

No tengo buenas respuestas a lo anterior.Pero parece que el software no se puede probar porque es arte y no ciencia.¿Cómo se prueba un Picasso?

Solución

Las pruebas son programas.

La verificación formal de los programas es un área de investigación enorme . (Ver, por ejemplo, el grupo en Carnegie Mellon .)

Se han verificado muchos programas complejos; por ejemplo, vea este núcleo escrito en Haskell .

Otros consejos

Los programas absolutamente pueden demostrarse que son correctos. Los programas pésimos son difíciles de probar. Para hacerlo incluso razonablemente bien, debe evolucionar el programa y realizar pruebas de la mano.

No puede automatizar la prueba debido al problema de detención. Sin embargo, puede probar manualmente las condiciones posteriores y las condiciones previas de cualquier declaración arbitraria o secuencia de declaraciones.

Debe leer Una disciplina de programación de Dijsktra.

Entonces, debe leer La ciencia de la programación de Gries.

Entonces sabrás cómo probar que los programas son correctos.

Solo un pequeño comentario para aquellos que mencionaron lo incompleto: no es el caso de todos los sistemas axiomáticos, solo los suficientemente potentes .

En otras palabras, Godel demostró que un sistema axiomático lo suficientemente poderoso como para describirse a sí mismo sería necesariamente incompleto. Sin embargo, esto no significa que sería inútil, y como otros se han vinculado, se han realizado varios intentos de pruebas del programa.

El doble problema (escribir programas para verificar pruebas) también es muy interesante.

De hecho, puede escribir programas probablemente correctos. Microsoft, por ejemplo, ha creado una extensión del lenguaje C # llamada Spec # que incluye un probador de teoremas automatizado. Para java, hay ESC / java . Estoy seguro de que hay muchos más ejemplos por ahí.

( edit : aparentemente la especificación # ya no se está desarrollando, pero las herramientas del contrato pasarán a formar parte de .NET 4.0 )

Veo algunos carteles saludando a mano sobre el problema de detención o teoremas de incompletitud que supuestamente impiden la verificación automática de programas. Por supuesto que esto no es cierto; estos problemas simplemente nos dicen que es posible escribir programas que no puedan ser correctos o incorrectos . Eso no nos impide construir programas que son demostrablemente correctos.

El problema de detención solo muestra que hay programas que no se pueden verificar. Una pregunta mucho más interesante y práctica es qué clase de programas pueden ser verificados formalmente. Tal vez todos los programas que le importan podrían (en teoría) ser verificados. ~~En la práctica, hasta ahora, solo se ha demostrado que los programas muy pequeños son correctos.~~

Si está realmente interesado en el tema, permítame recomendarle primero " The Science of Programming " ;, de David Gries, un clásico trabajo introductorio sobre el tema.

En realidad, es posible probar que los programas son correctos hasta cierto punto. Puede escribir condiciones previas y condiciones posteriores y luego demostrar que dado un estado que cumple con las condiciones previas, el estado resultante después de la ejecución cumplirá con las condiciones posteriores.

Donde se pone difícil, sin embargo, son los bucles. Para estos, adicionalmente necesita encontrar un bucle invariante y para mostrar la terminación correcta necesita encontrar una función de límite superior en el número máximo posible de iteraciones restantes después de cada bucle. También debe poder demostrar que esto disminuye al menos una vez después de cada iteración a través del ciclo.

Una vez que tenga todo esto para un programa, la prueba es mecánica. Pero desafortunadamente, no hay forma de derivar automáticamente las funciones invariantes y ligadas para los bucles. La intuición humana es suficiente para casos triviales con pequeños bucles, pero de manera realista, los programas complejos se vuelven rápidamente intratables.

Primero, ¿por qué dices " los programas NO PUEDEN ser probados " ;?

¿Qué quieres decir con " programas " de todos modos?

Si por programas te refieres a algoritmos, ¿no conoces los de Kruskal? Dijkstra's? MST? Prim's? ¿Búsqueda binaria? Mergesort? DP? Todas esas cosas tienen modelos matemáticos que describen sus comportamientos.

DESCRIBE. Las matemáticas no explican el por qué de las cosas, simplemente dibuja una imagen del cómo. No puedo demostrarte que el Sol saldrá mañana en el Este, pero puedo mostrarte los datos donde ha estado haciendo eso en el pasado.

Dijiste: " Si escribe un programa de computadora, ¿cómo es que puede tomar trabajos probados anteriores y usarlos para mostrar la verdad de su programa? No puedes, ya que no existe ninguno & Quot;

Espera? Usted no puede http://en.wikipedia.org/wiki/Algorithm#Algorithmic_analysis

No puedo mostrarte " verdad " Soy un programa tanto como no puedo mostrarte & Quot; verdad & Quot; en lenguaje. Ambas son representaciones de nuestra comprensión empírica del mundo. No en & Quot; verdad & Quot ;. Dejando a un lado todos los galimatías, puedo demostrarte matemáticamente que un algoritmo de combinación ordena los elementos en una lista con rendimiento O (nlogn), que un Dijkstra encontrará el camino más corto en un gráfico ponderado o que el algoritmo de Euclid te encontrará el mejor divisor común entre dos números. La & Quot; verdad en mi programa & Quot; en ese último caso, tal vez te encuentre el mayor divisor común entre dos números, ¿no crees?

Con una ecuación de recurrencia puedo delinearle cómo funciona su programa Fibonacci.

Ahora, ¿es la programación de computadoras un arte? Estoy seguro de que lo es. Tanto como las matemáticas.

No tengo experiencia en matemáticas, así que perdonen mi ignorancia, pero ¿qué significa "probar un programa"?¿Qué estás demostrando?¿La corrección?La corrección es una especificación que el programa debe verificar para que sea "correcta".Pero esta especificación la decide un humano, y ¿cómo se verifica que esta especificación sea correcta?

En mi opinión, hay errores en el programa porque los humanos tienen dificultades para expresar lo que realmente quieren.texto alternativo http://www.processdevelopers.com/images/PM_Build_Swing.gif

Entonces, ¿qué estás demostrando?¿Errores causados por falta de atención?

Además, ¿cuáles son los axiomas de la programación? ¿Las verdades muy atómicas del campo?

He TA'ed un curso llamado Programación basada en contratos (página de inicio del curso: http: // www.daimi.au.dk/KBP2/ ). Aquí lo que puedo extrapolar del curso (y otros cursos que he tomado)

Debe definir formalmente (matemáticamente) la semántica de su idioma. Pensemos en un lenguaje de programación simple; uno que solo tiene variables globales, ints, int arrays, aritmética, if-then-else, while, task y do-nothing [probablemente pueda usar un subconjunto de cualquier lenguaje principal como " implementación " ; de esto].

Un estado de ejecución sería una lista de pares (nombre de la variable, valor de la variable). Lea & Quot; {Q1} S1 {Q2} & Quot; como " la instrucción de ejecución S1 lo lleva del estado de ejecución Q1 al estado Q2 " ;.

Un axioma sería "if both {Q1} S1 {Q2} and {Q2} S2 {Q3}, then {Q1} S1; S2 {Q3}". Es decir, si la declaración S1 lo lleva del estado Q1 a Q2, y la declaración S2 lo lleva de Q2 a Q3, entonces & Quot; S1; S2 & Quot; (S1 seguido de S2) lo lleva del estado Q1 al estado Q3.

Otro axioma sería "if {Q1 && e != 0} S1 {Q2} and {Q1 && e == 0} S2 {Q2}, then {Q1} if e then S1 else S2 {Q2}".

Ahora, un poco de refinamiento: los Qn en {} 'serían en realidad declaraciones sobre estados, no estados en sí mismos.

Suponga que M (out, A1, A2) es una declaración que combina dos matrices ordenadas y almacena el resultado en out, y que todas las palabras que uso en el siguiente ejemplo se expresaron formalmente (matemáticamente). Entonces "{sorted(A1) && sorted(A2)} A := M(A1, A2) {sorted(A) && permutationOf(A, A1 concatened with A2)}" es la afirmación de que M implementa correctamente el algoritmo de fusión.

Uno puede intentar probar esto usando los axiomas anteriores (probablemente se necesitarán otros. Es probable que necesite un bucle, por ejemplo).

Espero que esto ilustre un poco cómo se verían los programas de prueba correctos. Y confía en mí: se necesita un lote de trabajo, incluso para algoritmos aparentemente simples, para demostrar que son correctos. Lo sé, leí muchos intentos ;-)

[si lees esto: tu entrega estuvo bien, son los otros los que me causaron dolores de cabeza ;-)]

Por supuesto que pueden, como otros han publicado.

Probar una subrutina muy pequeña correcta es un buen ejercicio que, en mi humilde opinión, todos los estudiantes de pregrado en un programa de grado relacionado con la programación deben hacer required . Le brinda una gran perspectiva para pensar cómo hacer que su código sea claro, fácil de revisar y mantener.

Sin embargo, en el mundo real es de uso práctico limitado.

Primero, así como los programas tienen errores, también las pruebas matemáticas. ¿Cómo probar que una prueba matemática es realmente correcta y no tiene ningún error? No puedes Y, por ejemplo, a cualquier número de pruebas matemáticas publicadas se les han descubierto errores, a veces años después.

Segundo, no puede probar que un programa es correcto sin tener 'a priori' una definición inequívoca de lo que se supone que debe hacer el programa. Pero cualquier definición inequívoca de lo que se supone que debe hacer un programa es un programa. (Aunque puede ser un programa en algún tipo de lenguaje de especificación para el que no tiene un compilador). Por lo tanto, antes de que pueda probar que un programa es correcto, primero debe tener otro programa que sea equivalente y conocido de antemano ser correcto. Entonces QED todo es inútil.

Recomendaría rastrear el clásico " No Silver Bullet " artículo de Brooks.

Hay mucha investigación en esta área ... como han dicho otros, las construcciones dentro del lenguaje de un programa son complejas, y esto solo empeora cuando se intenta validar o probar cualquier entrada.

Sin embargo, muchos idiomas permiten especificaciones, sobre qué entradas son aceptables (condiciones previas), y también permiten especificar el resultado final (condiciones posteriores).

Tales lenguajes incluyen: B, Evento B, Ada, fortran.

Y, por supuesto, hay muchas herramientas que están diseñadas para ayudarnos a probar ciertas propiedades sobre los programas. Por ejemplo, para demostrar la libertad de un punto muerto, uno podría procesar su programa a través de SPIN.

También hay muchas herramientas que también nos ayudan a detectar errores lógicos. Esto se puede hacer mediante análisis estático (goanna, satabs) o ejecución real de código (gnu valgrind?).

Sin embargo, no existe una herramienta única que realmente permita probar un programa completo, desde el inicio (especificación), implementación y despliegue. El método B se acerca, pero su verificación de implementación es muy muy débil. (Se supone que los humanos son infalibles en la traducción de la especificación a la implicación).

Como nota al margen, cuando utilice el método B, con frecuencia se encontrará construyendo pruebas complejas a partir de axiomas más pequeños. (Y lo mismo se aplica para otros demostradores de teoremas exhaustivos).

Ellos pueden. Pasé muchas, muchas horas como estudiante de primer año de la universidad haciendo pruebas de corrección del programa.

La razón por la que no es práctico en una escala macro es que escribir una prueba de un programa tiende a ser mucho más difícil que escribir el programa. Además, los programadores de hoy tienden a construir sistemas, no a escribir funciones o programas.

En una microescala, a veces lo hago mentalmente para funciones individuales, y tiendo a organizar mi código para facilitar su verificación.

Hay un famoso artículo sobre el software del transbordador espacial. Hacen pruebas, o algo equivalente. Es increíblemente costoso y consume mucho tiempo. Es posible que ese nivel de verificación sea necesario para ellos, pero para cualquier tipo de empresa de software comercial o de consumo, con las técnicas actuales, un competidor le ofrecerá su almuerzo y le ofrecerá una solución del 99.9% al 1% del costo. Nadie va a pagar $ 5000 por una MS Office que sea marginalmente más estable.

Si busca confianza, la alternativa a los programas de prueba es probarlos. Esto es más fácil de entender y puede automatizarse. También permite la clase de programas para los que las pruebas no son matemáticamente posibles, como se describió anteriormente.

Sobre todo, ninguna prueba es un sustituto para aprobar las pruebas de aceptación: *

El hecho de que un programa realmente haga lo que dice que hace, no significa que haga lo que el usuario quiere que haga.
- A menos que pueda probar que lo que dice que hace es lo que el usuario dice que quiere.
  - Lo que tienes que demostrar es lo que realmente quieren , porque, como usuarios, casi con certeza no saben lo que quieren. etc. Reductio ad absurdum.

* sin mencionar unidad, cobertura, funcional, integración y todos los otros tipos de pruebas.

Espero que esto te ayude en tu camino.

Algo que no se ha mencionado aquí es el B - Método que es un Sistema formal basado en métodos. Se utilizó para desarrollar el sistema de seguridad del metro de París. Hay herramientas disponibles para admitir el desarrollo B y Evento B, en particular Rodin .

No solo puede probar programas, también puede dejar que su computadora construya programas a partir de pruebas. Consulte Coq . Por lo tanto, ni siquiera tiene que preocuparse por la posibilidad de haber cometido un error en su implementación.

Teoremas de Godel a pesar de ... ¿Cuál sería el punto? ? ¡Qué simplista & Quot; verdades & Quot; te gustaria probar ¿Qué te gustaría derivar de esas verdades? Si bien puedo comer estas palabras ... ¿dónde está la practicidad?

Los programas PUEDEN ser probados. Es fácil y sencillo si los escribe en un lenguaje como, por ejemplo, ML estándar de Nueva Jersey (SML / NJ).

Su declaración es amplia, por lo que captura muchos peces.

La conclusión es: algunos programas definitivamente pueden probarse correctos. Todos los programas pueden no probarse correctos.

Aquí hay un ejemplo trivial que, fíjate, es exactamente el mismo tipo de prueba que destruyó la teoría de conjuntos en el pasado: crea un programa que pueda determinar si es correcto, y si encuentra que es correcto, da una respuesta incorrecta.

Esto es G & # 246; teorema de del, simple y llanamente.

Pero esto no es tan problemático, ya que podemos probar muchos programas.

Asumamos un lenguaje puramente funcional (es decir, Haskell). Los efectos secundarios se pueden tener muy en cuenta en estos idiomas.

Probar que un programa produce el resultado correcto requiere que especifique:

una correspondencia entre tipos de datos y conjuntos matemáticos
una correspondencia entre las funciones de Haskell y las funciones matemáticas
un conjunto de axiomas que especifican qué funciones puede construir a partir de otros, y la construcción correspondiente en el lado matemático.

Este conjunto de especificaciones se denomina semántica denotacional . Le permiten probar la razón sobre los programas que usan las matemáticas.

La buena noticia es que la estructura " de los programas " (punto 3 anterior) y la estructura & "de conjuntos matemáticos &"; son bastante similares (la palabra de moda es topos o categoría cerrada cartesiana ), por lo que 1 / las pruebas que realice en el lado matemático se transferirán fácilmente a construcciones programáticas 2 / el los programas que escribe se muestran fácilmente como matemáticamente correctos.

Lea sobre el problema de detención (que trata sobre la dificultad de probar algo tan simple como si un programa se completa o no). Fundamentalmente, el problema está relacionado con el teorema de incompletitud de G & # 246; del.

Algunas partes de los programas se pueden probar. Por ejemplo, el compilador de C # que verifica estáticamente y garantiza la seguridad del tipo, si la compilación tiene éxito. Pero sospecho que el núcleo de su pregunta es demostrar que un programa funciona correctamente. Se puede probar que muchos (no me atrevo a decir la mayoría) algoritmos son correctos, pero un programa completo probablemente no se puede probar estáticamente debido a lo siguiente:

La verificación requiere que se atraviesen todas las ramas posibles (llamadas, ifs e interrupciones), que en el código de programa avanzado tiene una complejidad de tiempo supercúbica (por lo tanto, nunca se completará en un tiempo razonable).
Algunas técnicas de programación, ya sea mediante la creación de componentes o el uso de la reflexión, hacen que sea imposible predecir estáticamente la ejecución del código (es decir, no sabe cómo otro programador usará su biblioteca, y el compilador tiene dificultades para predecir cómo la reflexión en un consumidor invocará la funcionalidad.

Y esos son solo algunos ...

Si el programa tiene un objetivo bien definido y supuestos iniciales (ignorando el Gódel ...) puede probarse. Encuentre todos los números primos, x, para 6 & Lt; = x & Lt; = 10, su respuesta es 7 y eso se puede probar. Escribí un programa que reproduce NIM (el primer programa de Python Alguna vez escribí) y, en teoría, la computadora siempre gana después de que el juego cae en un estado en el que la computadora puede ganar. No he podido demostrar que sea cierto, pero ES cierto (matemáticamente por una prueba de suma binaria digital), creo que a menos que haya cometido un error en el código. ¿Cometí un error, no en serio, alguien me puede decir si este programa es vencible?

Hay algunos teoremas matemáticos que han sido " probados " con código de computadora como el teorema de cuatro colores . Pero hay objeciones, porque como dijiste, ¿puedes probar el programa?

Además, ¿cuáles son los axiomas de la programación? ¿Las verdades muy atómicas del campo?

¿Son los códigos de operación las " verdades atómicas " ;? Por ejemplo al ver ...

mov ax,1

... ¿no podría un programador afirmar como axiomático que, salvo un problema de hardware, después de ejecutar esta declaración, el registro ax de la CPU ahora contendría 1?

Si escribe un programa de computadora, ¿cómo es que puede tomar trabajos probados anteriores y usarlos para mostrar la verdad de su programa?

El " trabajo previo " entonces podría ser el entorno de tiempo de ejecución en el que se ejecuta el nuevo programa.

El nuevo programa se puede probar: además de las pruebas formales, se puede probar " mediante inspección " y por varias formas de " probar " (incluyendo " pruebas de aceptación ").

¿Cómo se prueba un Picasso?

Si el software se parece más al diseño industrial o la ingeniería que al arte, una mejor pregunta podría ser " ¿cómo se prueba un puente o un avión? "

probar que un programa es correcto solo se puede hacer en relación con la especificación del programa; es posible pero costoso / consume mucho tiempo

algunos sistemas CASE producen programas más susceptibles a pruebas que otros, pero nuevamente, esto se basa en una semántica formal de la especificación ...

... y entonces, ¿cómo demuestras que la especificación es correcta? ¡Correcto! ¡Con más especificaciones!

Leí un poco sobre esto, pero hay dos problemas.

Primero, no puedes probar algo abstracto llamado corrección. Puede, si las cosas están configuradas correctamente, demostrar que dos sistemas formales son equivalentes. Puede probar que un programa implementa un conjunto de especificaciones, y es más fácil hacerlo construyendo la prueba y el programa más o menos en paralelo. Por lo tanto, las especificaciones deben ser lo suficientemente detalladas para proporcionar algo contra lo que probar, y por lo tanto, la especificación es efectivamente un programa . El problema de escribir un programa para satisfacer un propósito se convierte en el problema de escribir una especificación formal detallada de un programa para satisfacer un propósito, y eso no es necesariamente un paso adelante.

Segundo, los programas son complicados. También lo son las pruebas de corrección. Si puede cometer un error al escribir un programa, seguramente puede probarlo. Dijkstra y Gries me dijeron, esencialmente, que si yo fuera un matemático perfecto, podría ser un buen programador. El valor aquí es que probar y programar son dos procesos de pensamiento algo diferentes, y al menos en mi experiencia cometo diferentes tipos de errores.

En mi experiencia, probar programas no es inútil. Cuando intento hacer algo que puedo describir formalmente, probar que la implementación es correcta elimina una gran cantidad de errores difíciles de encontrar, principalmente dejando los tontos, que puedo detectar fácilmente en las pruebas. En un proyecto que debe producir código extremadamente libre de errores, puede ser un complemento útil. No es adecuado para todas las aplicaciones, y ciertamente no es una bala de plata.

Como otros señalaron, (algunos) programas pueden ser probados.

Sin embargo, un problema en la práctica es que primero necesita algo (es decir, una suposición o un teorema) que desea probar. Entonces, para probar algo sobre un programa, primero necesita una descripción formal de lo que debe hacer (por ejemplo, antes y después de las condiciones).

En otras palabras, necesita una especificación formal del programa. Pero obtener incluso una especificación razonable (mucho menos rigurosa formal) ya es una de las cosas más difíciles en el desarrollo de software. Por lo tanto, generalmente es muy difícil demostrar cosas interesantes sobre un programa (del mundo real).

Sin embargo, hay algunas cosas que pueden (y han sido) formalizarse más fácilmente (y demostrarse). Si al menos puede probar que su programa no se bloqueará, eso ya es algo :-).

Por cierto, algunas advertencias / errores del compilador son pruebas esencialmente (simples) sobre un programa. Por ejemplo, el compilador de Java demostrará que nunca accede a una variable no inicializada en su código (de lo contrario, le dará un error de compilador).

No he leído todas las respuestas, pero tal como lo veo, probar los programas no tiene sentido, por eso nadie lo hace.

Si tiene un proyecto relativamente pequeño / mediano (digamos, 10K líneas de código), entonces la prueba probablemente será también 10k líneas, si no más.

Piénselo, si el programa puede tener errores, la prueba también puede tener " bugs " ;. ¡Quizás necesites una prueba para la prueba!

Otra cosa a considerar, los programas son muy muy formales y precisos. No puede ser más riguroso y formal, porque el código del programa debe ser ejecutado por una máquina muy tonta.

Si bien las pruebas serán leídas por humanos, entonces tienden a ser menos rigurosas que el código real.

Lo único que querrá probar son los algoritmos de bajo nivel que operan en estructuras de datos específicas (por ejemplo, clasificación rápida, inserción en un árbol binario, etc.).

Estas cosas son algo complicadas, no es inmediatamente obvio por qué funcionan y / o si siempre funcionarán. También son bloques de construcción básicos para todos los demás programas.

La mayoría de las respuestas se centraron en la práctica y eso está bien: en la práctica no te importa la prueba formal. Pero, ¿qué hay en teoría?

Los programas se pueden probar de la misma manera que una declaración matemática. ¡Pero no en el sentido que quisiste decir! ¡En cualquier marco potente suficiente, hay enunciados matemáticos (y programas) que no se pueden probar! Ver aquí

Mucho ruido aquí, pero de todos modos voy a gritar al viento ...

" Probar correcto " tiene diferentes significados en diferentes contextos. En sistemas formales , & Quot; demuestre que es correcto & Quot; significa que una fórmula puede derivarse de otras fórmulas probadas (o axiomáticas). " Probar correcto " en programación simplemente muestra que el código es equivalente a una especificación formal. Pero, ¿cómo demuestras que la especificación formal es correcta? Lamentablemente, no hay forma de mostrar una especificación libre de errores o una solución a un problema del mundo real que no sea mediante pruebas.

Solo mis 2 centavos, que se suman a las cosas interesantes que ya existen.

De todos los programas que no se pueden probar, los más comunes son aquellos que realizan IO (alguna interacción impredecible con el mundo o los usuarios). Incluso las pruebas automatizadas a veces simplemente olvidan que & Quot; probado & Quot; programas " ejecutar en algún hardware físico, no el ideal descrito por el modelo.

Por otro lado, a las pruebas matemáticas no les importa mucho el mundo. Una pregunta recurrente con Maths es si describe algo real. Se plantea cada vez que se inventa algo nuevo, como números imaginarios o espacios no euclidianos. Entonces se olvida la pregunta, ya que estas nuevas teorías son herramientas tan buenas. Como un buen programa, simplemente funciona.

Licenciado bajo: CC-BY-SA con atribución

No afiliado a StackOverflow