math - ¿Por qué los programas no pueden ser probados?
theory proof (30)
¿Por qué un programa de computadora no puede probarse solo como una declaración matemática? Una prueba matemática se construye sobre otras pruebas, que se construyen a partir de aún más pruebas y hasta axiomas - esas verdades verdades que tenemos como evidente.
Los programas de computadora no parecen tener tal estructura. 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 ninguno existe. Además, ¿cuáles son los axiomas de la programación? ¿Las verdades atómicas del campo?
No tengo buenas respuestas a lo anterior. Pero parece que el software no puede ser probado porque es arte y no ciencia. ¿Cómo demuestras ser un Picasso?
Además, ¿cuáles son los axiomas de la programación? ¿Las verdades 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 del ax 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 anterior" podría ser el entorno de tiempo de ejecución en el que se ejecuta el nuevo programa.
El nuevo programa puede ser probado: aparte de las pruebas formales, puede ser probado "por inspección" y por varias formas de "prueba" (incluyendo "pruebas de aceptación").
¿Cómo demuestras ser un Picasso?
Si el software se parece más al diseño o ingeniería industrial que al arte, una mejor pregunta podría ser "¿cómo se puede probar que es un puente o un avión?"
Además, ¿cuáles son los axiomas de la programación? ¿Las verdades atómicas del campo?
He recibido un curso de TA llamado Programación basada en contrato (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)
Tienes que definir formalmente (matemáticamente) la semántica de tu lenguaje. Pensemos en un lenguaje de programación simple; uno que solo tiene variables globales, ints, int arrays, aritmética, if-then-else, while, assignment y do-nothing [es probable que pueda usar un subconjunto de cualquier lengua mainstream como una "implementación" de esto].
Un estado de ejecución sería una lista de pares (nombre de la variable, valor de la variable). Lea "{Q1} S1 {Q2}" ya que "la instrucción de ejecución S1 lo lleva del estado de ejecución Q1 al estado Q2".
Un axioma sería entonces "if both {Q1} S1 {Q2} and {Q2} S2 {Q3}, then {Q1} S1; S2 {Q3}" . Es decir, si la instrucción S1 te lleva del estado Q1 al Q2, y la instrucción S2 te lleva de Q2 a Q3, entonces "S1; S2" (S1 seguido de S2) te 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 {} ''s serían en realidad declaraciones sobre estados, no estados en sí mismos.
Supongamos que M (out, A1, A2) es una declaración que fusiona dos matrices ordenadas y almacena el resultado, 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 tratar de probar esto usando los axiomas anteriores (probablemente se necesitarán algunos otros. Es probable que necesite un bucle, para uno).
Espero que esto ilustre un poco de lo que los programas de prueba podrían ser correctos. Y créeme: se necesita mucho trabajo, incluso para algoritmos aparentemente simples, para probar que son correctos. Lo sé, leo muchos intentos ;-)
[si lees esto: tu hand-in estuvo bien, son todos los otros los que me causaron dolores de cabeza ;-)]
Algunas partes de los programas pueden ser probados. Por ejemplo, el compilador de C # que verifica y garantiza estáticamente la seguridad de 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 algoritmos (no me atrevo a decir que la mayoría) son correctos, pero es probable que un programa completo no pueda demostrarse estáticamente debido a lo siguiente:
- La verificación requiere que se atraviesen todas las ramas posibles (llamadas, si e interrupciones), lo 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, imposibilitan predecir estáticamente la ejecución del código (es decir, no se sabe cómo utilizará su biblioteca otro programador y el compilador tiene dificultades para predecir cómo se reflejará el reflejo en un consumidor invocar la funcionalidad.
Y esos son solo algunos ...
Como otros señalaron, (algunos) programas pueden ser probados.
Sin embargo, uno de los problemas en la práctica es que primero necesita algo (es decir, una suposición o un teorema) que quiera probar. Entonces, para probar algo acerca de un programa, primero necesita una descripción formal de lo que debería hacer (por ejemplo, condiciones previas y posteriores).
En otras palabras, necesita una especificación formal del programa. Pero obtener incluso una especificación razonable (mucho menos rigurosa) ya es una de las cosas más difíciles en el desarrollo de software. Por lo tanto, en general es muy difícil demostrar cosas interesantes sobre un programa (del mundo real).
Sin embargo, hay algunas cosas que pueden ser (y han sido) más fácilmente formalizadas (y probadas). 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 probará que nunca accede a una variable no inicializada en su código (de lo contrario, le dará un error de compilación).
De hecho, puede escribir programas provablemente correctos. Microsoft, por ejemplo, ha creado una extensión del lenguaje C # llamada Spec# que incluye un demostrador de teoremas automatizado. Para Java, hay ESC/java . Estoy seguro de que hay muchos más ejemplos por ahí.
( edit : aparentemente spec # ya no se está desarrollando, pero las herramientas del contrato formarán parte de .NET 4.0 )
Veo algunos carteles agitando la mano sobre el problema de detención o los teoremas de incompletitud que supuestamente impiden la verificación automática de los programas. Por supuesto que esto no es cierto; estos problemas simplemente nos dicen que es posible escribir programas que no se puede probar que sean correctos o incorrectos . Eso no nos impide construir programas que sean probablemente correctos.
El problema de detención solo muestra que hay programas que no se pueden verificar. Una pregunta mucho más interesante y más práctica es qué clase de programas se puede verificar formalmente. Quizás cada programa que a alguien le importe podría (en teoría) ser verificado. En la práctica, hasta ahora, solo los programas muy pequeños han demostrado ser correctos.
Ellos pueden. Pasé muchas, muchas horas como estudiante de primer año de universidad haciendo pruebas de corrección del programa.
La razón por la cual no es práctico a 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 hoy en día tienden a construir sistemas, no a escribir funciones o programas.
A escala micro, a veces lo hago mentalmente para funciones individuales, y tiendo a organizar mi código para que sea fácil de verificar.
Hay un artículo famoso sobre el software del transbordador espacial. Hacen pruebas, o algo equivalente. Es increíblemente costoso y lleva mucho tiempo. Ese nivel de verificación puede ser necesario para ellos, pero para cualquier tipo de empresa de software comercial o de consumo, con las técnicas actuales, un competidor que le ofrece una solución al 99,9% al 1% del costo le hará comer. Nadie va a pagar $ 5000 por una MS Office que sea marginalmente más estable.
Hay mucha investigación en esta área ... como otros han dicho, los constructos dentro de un lenguaje de programa son complejos, y esto solo empeora, al intentar validar o probar cualquier entrada dada.
Sin embargo, muchos lenguajes permiten especificaciones, sobre qué entradas son aceptables (precondiciones), y también permiten especificar el resultado final (condiciones de publicación).
Tales idiomas incluyen: B, Evento B, Ada, fortran.
Y, por supuesto, hay muchas herramientas que están diseñadas para ayudarnos a probar ciertas propiedades de los programas. Por ejemplo, para probar la libertad de estancamiento, uno podría reducir su programa a través de SPIN.
También hay muchas herramientas que también nos ayudan a detectar errores de lógica. Esto se puede hacer a través de un análisis estático (goanna, satabs) o la ejecución real del código (gnu valgrind?).
Sin embargo, no existe una herramienta que realmente permita probar un programa completo, desde el inicio (especificación), la implementación y la implementación. El método B se acerca, pero su verificación de implementación es muy débil. (Supone que los humanos son infalibles en la traducción de speicficaiton a implmentation).
Como nota al margen, al usar el método B, con frecuencia te encontrarás construyendo pruebas complejas a partir de axiomas más pequeños. (Y lo mismo se aplica a otros demostradores de teoremas exhasustivos).
La mayoría de las respuestas se centraron en la práctica y está bien: en la práctica, no te importan las pruebas formales. Pero, ¿qué es en teoría?
Los programas pueden ser probados tal como lo puede hacer una declaración matemática. ¡Pero no en el sentido que quisiste decir! ¡En cualquier marco suficientemente poderoso, hay enunciados matemáticos (y programas) que no pueden ser probados! Mira aquí
Las pruebas are programas.
La verificación formal de los programas es un área de investigación enorme . (Ver, por ejemplo, el grupo en Carnegie Mellon .)
Muchos programas complejos han sido verificados; por ejemplo, vea este kernel escrito en Haskell .
Leí un poco sobre esto, pero hay dos problemas.
Primero, no puedes probar algo abstracto llamado corrección. Si las cosas están configuradas correctamente, puede probar 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 suficientemente detalladas para proporcionar algo contra lo que demostrar, 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.
En segundo lugar, 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 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, hago diferentes tipos de errores.
En mi experiencia, probar programas no es inútil. Cuando trato de hacer algo que puedo describir formalmente, probar que la implementación correcta elimina un montón de errores difíciles de encontrar, principalmente dejando a 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.
Lea sobre el problema de detención (que es 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ödel.
Los programas PUEDEN ser probados. Es muy fácil si los escribe en un lenguaje como, por ejemplo, el Estándar ML de Nueva Jersey (SML / NJ).
Los programas absolutamente pueden ser probados. Los programas pésimos son difíciles de probar. Para hacerlo incluso razonablemente bien, debe evolucionar el programa y la prueba 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.
Debes leer la Disciplina de Programación de Dijsktra.
Luego, debes leer La ciencia de la programación de Gries.
Entonces sabrá cómo probar que los programas son correctos.
No he leído todas las respuestas, pero la forma en que lo veo, probar programas no tiene sentido, es por eso que nadie lo hace.
Si tienes un proyecto relativamente pequeño / mediano (digamos, 10K líneas de código), entonces la prueba probablemente sea también de 10k líneas, si no más.
Piénselo, si el programa puede tener errores, la prueba también puede tener "errores". ¡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.
Las únicas cosas que querrá probar son algoritmos de bajo nivel que operan en estructuras de datos específicas (por ejemplo, quicksort, 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 el resto del software.
No solo puede probar programas, puede dejar que su computadora construya programas a partir de pruebas. Ver Coq . Entonces, ni siquiera tiene que preocuparse por la posibilidad de haber cometido un error en su implementación.
No soy de origen matemático, así que perdona mi ignorancia, pero ¿qué significa "probar un programa"? ¿Qué estás probando? La corrección? La corrección es una especificación que el programa debe verificar para ser "correcta". Pero esta especificación es decidida por un humano, y ¿cómo se verifica que esta especificación es 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 probando? ¿Errores causados por la falta de atención?
Por supuesto que pueden, como otros han publicado.
Probar que una subrutina muy pequeña sea correcta es un buen ejercicio que, en mi humilde opinión, todos los estudiantes de pregrado de un programa de grado relacionado con la programación deben realizar. Le da una gran idea sobre 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 lo hacen 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 contraejemplo, cualquier número de pruebas matemáticas publicadas ha tenido errores descubiertos en ellas, a veces años después.
En segundo lugar, no puede probar que un programa es correcto sin tener ''a priori'' una definición inequívoca de lo que el programa debe hacer. 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 que se conozca de antemano. ser correcto. Entonces QED todo es inútil.
Recomendaría buscar el clásico artículo " No Silver Bullet " de Brooks.
Primero, ¿por qué dice "los programas NO PUEDEN probarse"?
¿Qué quiere decir con "programas" de todos modos?
Si por programas quieres algoritmos, ¿no conoces los de Kruskal? Dijkstra es? MST? ¿Prim? ¿Búsqueda binaria? Mergesort? DP? Todas esas cosas tienen modelos matemáticos que describen sus comportamientos.
DESCRIBIR. Las matemáticas no explican el porqué de las cosas, simplemente dibuja una imagen del cómo. No puedo demostrarte que el Sol se levantará mañana en el Este, pero puedo mostrar los datos donde ha estado haciendo eso en el pasado.
Usted dijo: "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 puede existir ninguno"
¿Espere? NO PUEDES? http://en.wikipedia.org/wiki/Algorithm#Algorithmic_analysis
No puedo mostrarle "la verdad" en un programa tanto como no puedo mostrarle "la verdad" en el lenguaje. Ambas son representaciones de nuestra comprensión empírica del mundo. No en "verdad". Dejando de lado todo el galimatías puedo demostrarles matemáticamente que un algoritmo mergesort clasificará los elementos en una lista con el rendimiento O (nlogn), que un Dijkstra encontrará la ruta más corta en un gráfico ponderado, o que el algoritmo de Euclides lo encontrará el mejor divisor común entre dos números. La "verdad en mi programa" 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 delinear cómo funciona tu programa Fibonacci.
Ahora, ¿la programación de computadoras es un arte? Yo creo que es así. Tanto como las matemáticas.
Si busca confianza, la alternativa de probar programas los está probando. 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.
Por encima de todo, ninguna prueba es un sustituto de pasar las pruebas de aceptación: *
Solo porque un programa realmente haga lo que dice, no significa que haga lo que el usuario quiere que haga.
A menos que pueda demostrar que lo que dice es lo que el usuario dice que quiere.
- Lo que tienes que probar es lo que realmente quieren , ya que, como usuario, casi seguro que 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.
Si el programa tiene un objetivo bien definido y suposiciones iniciales (ignorando Godel ...) puede ser probado. Encuentre todos los primos, x, para 6 <= x <= 10, su respuesta es 7 y eso puede ser probado. Escribí un programa que reproduce NIM (el primer programa de Python que 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 probarlo como cierto, pero ES verdad (matemáticamente por una prueba de suma binaria digital), creo, 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ódigos de computadora como el teorema de los cuatro colores . Pero hay objeciones, porque como dijiste, ¿puedes probar el programa?
Si realmente está interesado en el tema, permítame primero recomendar "The Science of Programming" de David Gries, un clásico trabajo introductorio sobre el tema.
De hecho, es posible demostrar que los programas son correctos en cierta medida. Puede escribir condiciones previas y posteriores y luego probar que, dado un estado que cumpla con las condiciones previas, el estado resultante después de la ejecución cumplirá las condiciones posteriores.
Sin embargo, donde se pone complicado es loops. Para estos, también 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 tienes todo esto para un programa, la prueba es mecánica. Pero desafortunadamente, no hay forma de derivar automáticamente las funciones invariables y enlazadas para 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.
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 los que realizan IO (alguna interacción impredecible con el mundo o los usuarios). Incluso las pruebas automatizadas a veces simplemente olvidan que los programas "comprobados" se ejecutan en algún hardware físico, no el ideal descrito por el modelo.
Por otro lado, las pruebas matemáticas no importan mucho en el mundo. Una pregunta recurrente con Maths es si describe algo real. Se levanta cada vez que se inventa algo nuevo como números imaginarios o espacio no euclidiano. Entonces la pregunta se olvida ya que estas nuevas teorías son tan buenas herramientas. Como un buen programa, simplemente funciona.
Solo un pequeño comentario para aquellos que mencionaron lo incompleto: no es el caso para todos los sistemas axiomáticos, solo los suficientemente poderosos .
En otras palabras, Godel demostró que un sistema axiomático lo suficientemente poderoso como para describirse a sí mismo sería necesariamente incompleto. Esto no significa que sería inútil, sin embargo, y como otros se han relacionado, se han realizado varios intentos de pruebas del programa.
El problema dual (escribir programas para verificar pruebas) también es muy interesante.
Su declaración es amplia, por lo que atrapa muchos peces.
La conclusión es: algunos programas definitivamente se pueden probar como correctos. Todos los programas no pueden ser probados correctamente.
Aquí hay un ejemplo trivial que, en su opinión, es exactamente el mismo tipo de prueba que destruyó la teoría de conjuntos en el día: crea un programa que puede determinar si él mismo es correcto y, si encuentra que es correcto, da una respuesta incorrecta.
Este es el teorema de Gödel, claro y simple.
Pero esto no es tan problemático, ya que podemos probar muchos programas.
Supongamos un lenguaje puramente funcional (es decir, Haskell). Los efectos secundarios pueden tomarse bastante en cuenta en dichos idiomas.
Para demostrar que un programa produce el resultado correcto, debe especificar:
- 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 especifica qué funciones se le permite construir a partir de otras y la construcción correspondiente en el lado matemático.
Este conjunto de especificaciones se denomina semántica de denotación . Le permiten probar la razón de los programas que usan las matemáticas.
La buena noticia es que la "estructura de 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 se hacen en el lado matemático se transferirá fácilmente a construcciones programáticas 2 / los programas que escribe se muestran fácilmente como matemáticamente correctos.
Tanto ruido aquí, pero voy a gritar en el viento de todos modos ...
"Demostrar correcto" tiene diferentes significados en diferentes contextos. En los sistemas formales , "demostrar que es correcto" significa que una fórmula puede derivarse de otras fórmulas probadas (o axiomáticas). "Demostrar correcto" en la 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 manera de mostrar una especificación para estar libre de errores o una solución de cualquier problema del mundo real que no sea a través de pruebas.
probar que un programa es correcto solo puede hacerse 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 las pruebas que otros, pero una vez más, esto se basa en una semántica formal de la especificación ...
... y entonces, ¿cómo demuestras que la especificación es correcta? ¡Derecha! ¡Con más especificaciones!
A pesar de los Teoremas de Godel ... ¿Cuál sería el punto? ¿Qué "verdades" simplistas te gustaría probar? ¿Qué te gustaría derivar de esas verdades? Si bien puedo comer estas palabras ... ¿dónde está la practicidad?