Programas teóricamente libres de errores

He leído muchos artículos que afirman que el código no puede estar libre de errores, y están hablando de estos teoremas:

• Problema de detención
• Teorema de incompletitud de Gödel
• Teorema de Rice

En realidad, el teorema de Rice parece una implicación del problema de detención y el problema de detención está en estrecha relación con el teorema de incompletitud de Gödel.

¿Esto implica que cada programa tendrá al menos un comportamiento no deseado? ¿O significa que no es posible escribir código para verificarlo? ¿Qué pasa con la verificación recursiva? Asumamos que tengo dos programas. Ambos tienen errores, pero no comparten el mismo error. ¿Qué pasará si los ejecuto simultáneamente?

Y, por supuesto, la mayoría de las discusiones hablaron sobre las máquinas de Turing. ¿Qué pasa con la automatización lineal (computadoras reales)?

No es tanto que los programas no puedan estar libres de errores; es que es muy difícil demostrar que lo son, si el programa que intenta probar no es trivial.

No por falta de intentos, eso sí. Se supone que los sistemas de tipos proporcionan cierta seguridad; Haskell tiene un sistema de tipos altamente sofisticado que hace esto, hasta cierto punto. Pero nunca puedes eliminar toda la incertidumbre.

Considere la siguiente función:

int add(int a, int b) { return a + b; }

¿Qué podría salir mal con esta función? Ya sé lo que estás pensando. Digamos que hemos cubierto todas las bases, como verificar el desbordamiento, etc. ¿Qué sucede si un rayo cósmico golpea el procesador y hace que se ejecute?

LaunchMissiles();

¿en lugar?

OK, tal vez eso sea un poco artificial. Pero incluso las funciones simples como la addfunción anterior deben operar en entornos donde el procesador cambia constantemente de contexto, cambiando entre múltiples hilos y núcleos. En un entorno como ese, cualquier cosa puede suceder. Si duda de esto, considere que la RAM es confiable, no porque esté libre de errores, sino porque tiene un sistema incorporado para corregir los errores de bits que inevitablemente ocurren.

Sé lo que estás pensando. "Pero estoy hablando de software, no de hardware".

Existen muchas técnicas que pueden mejorar su nivel de confianza de que el software funciona de la manera en que se supone que debe hacerlo. La programación funcional es una de ellas. La programación funcional le permite razonar mejor sobre la concurrencia. Pero la programación funcional no es una prueba, tampoco lo son las pruebas unitarias.

¿Por qué? Porque tienes estas cosas llamadas casos extremos.

Y una vez que solo superas un poco la simplicidad return a + b, se vuelve notablemente difícil probar la corrección de un programa.

Lecturas adicionales
Escriben las cosas correctas
La explosión de Ariane 5

Primero, establezcamos en qué contexto desea analizar esto. Las Preguntas y Respuestas de los Programadores en Stack Exchange sugieren que probablemente esté interesado en la existencia de herramientas / lenguajes en el mundo real en lugar de resultados teóricos y teoremas de Ciencias de la Computación .

He leído muchos artículos que dicen que el código no puede estar libre de errores

Espero que no, porque tal afirmación es incorrecta. Aunque se acepta comúnmente que la mayoría de las aplicaciones a gran escala no están libres de errores, según mi leal saber y entender.

Más comúnmente aceptado es que no existe (es decir, existencia, no posibilidad) una herramienta que determine perfectamente si un programa escrito en un Turing-complete lenguaje de programación está completamente libre de errores.

Una no prueba es una extensión intuitiva del problema de detención, combinada con los datos de observación de la experiencia cotidiana.

No hace el software existen que puede hacer "pruebas de corrección " que verificar que un programa cumple con los correspondientes formales especificaciones para el programa.

¿Esto implica que cada programa tendrá al menos un comportamiento no deseado?

No. Aunque se ha descubierto que la mayoría de las aplicaciones tienen al menos un error o un comportamiento no deseado.

¿O significa que no es posible escribir código para verificarlo?

No, puede usar especificaciones formales y asistentes de prueba para verificar que se cumplan las especificaciones , pero como la experiencia ha demostrado, los errores aún pueden existir en el sistema en general, como factores fuera de la especificación: el traductor de código fuente y el hardware, y con mayor frecuencia se cometen errores en las especificaciones mismas.

Para obtener más detalles sangrientos, vea Coq es una herramienta / lenguaje / sistema de este tipo.

¿Qué pasa con la verificación recursiva?

No lo sé. No estoy familiarizado con él, y no estoy seguro si es un problema de computabilidad o un problema de optimización del compilador.

Quiero preguntar, ¿implica que cada código tendrá al menos un comportamiento no deseado?

No. Los programas correctos pueden ser y están escritos. Eso sí, un programa puede ser correcto, pero su ejecución puede fallar debido, por ejemplo, a circunstancias físicas (como escribió el usuario Robert Harvey en su respuesta aquí ), pero este es un asunto distinto: el código de ese programa sigue siendo correcto. Para ser más precisos, la falla no es causada por una falla o error en el programa en sí, sino en la máquina subyacente que lo ejecuta (*).

(*) Estoy tomando prestadas definiciones de falla , error y falla del campo de confiabilidad como, respectivamente, un defecto estático, un estado interno incorrecto y un comportamiento externo incorrecto observado de acuerdo con su especificación (ver <cualquier documento de ese campo>) .

¿O significa que no puedo escribir código, que lo comprobará?

Consulte el caso general en la declaración anterior y está en lo correcto.

Es posible que pueda escribir un programa que verifique si un programa X específico es correcto. Por ejemplo, si define un programa "hola mundo" como uno con dos instrucciones en secuencia, a saber, print("hello world")y exit, puede escribir un programa que verifique si su entrada es un programa compuesto de estas dos instrucciones en secuencia, informando así si es un programa correcto "hola mundo" o no.

Lo que no puede hacer con las formulaciones actuales es escribir un programa para verificar si algún programa arbitrario se detiene, lo que implica la imposibilidad de probar la corrección en los casos generales.

Ejecutar dos o más variantes del mismo programa es una técnica bien conocida de tolerancia a fallas llamada programación de variante N (o versión N). Es un reconocimiento de la presencia de errores en el software.

Por lo general, estas variantes están codificadas por diferentes equipos de desarrollo, utilizando diferentes compiladores, y a veces se ejecutan en diferentes CPU con diferentes sistemas operativos. Los resultados se votan antes de ser enviados al usuario. Boeing y Airbus adoran este tipo de arquitectura.

Quedan dos enlaces débiles que conducen a errores de modo común:

• Solo hay una especificación.
• El sistema de votación es único o complejo.

Un programa tiene algunas especificaciones y se ejecuta en algún entorno.

^{(El ejemplo del rayo cósmico en otras respuestas cambiando adda FireMissiles podría considerarse parte del "ambiente")}

Suponiendo que puede especificar formalmente el comportamiento previsto del programa (es decir, su especificación) y su entorno, a veces podría probar formalmente que el programa está, en ese preciso sentido, libre de errores (por lo que su comportamiento o salida respeta la formalización de su especificación en la formalización de su entorno).

En particular, puede usar analizadores de fuente estática de sonido, como por ejemplo Frama-C .

^{(pero el estado actual de la técnica de tales analizadores no permite que todo programa de análisis y prueba de programas a gran escala como el compilador GCC o el navegador Firefox o el núcleo de Linux, y mi creencia es que tales pruebas no va a suceder en mi vida Nací en 1959)}

Sin embargo, lo que ha demostrado es el comportamiento correcto del programa con algunas especificaciones particulares en algunos (clase de) entornos.

Hablando en términos prácticos, podrías (y la NASA o la ESA probablemente quieran) probar que algunos programas de naves espaciales están "libres de errores" y que tienen una especificación precisa y formal. Pero eso no significa que su sistema siempre se comportará como usted quiere.

En palabras más simples, si su robot de nave espacial cumple con algún ET y no lo ha especificado, no hay forma de que su robot se comporte como realmente desea ...

Lea también las entradas de blog de J.Pitrat .

Por cierto, el problema de detención o el teorema de Gödel probablemente se aplica también al cerebro humano, o incluso a la especie humana.

¿Esto implica que cada programa tendrá al menos un comportamiento no deseado?

No.

El problema de detención dice que es imposible escribir un programa que pruebe si cada programa se detiene en un tiempo finito. Esto no significa que sea imposible escribir un programa que pueda clasificar algunos programas como detenidos, otros como no detenidos. Lo que significa es que siempre existirán algunos programas que un analizador de detención no puede clasificar de una forma u otra.

Los teoremas de incompletitud de Gödel tienen un área gris similar a ellos. Dado un sistema matemático de suficiente complejidad, existirán algunas declaraciones hechas en el contexto de ese sistema cuya veracidad no puede evaluarse. Esto no significa que los matemáticos tengan que renunciar a la idea de la prueba. La prueba sigue siendo la piedra angular de las matemáticas.

Se puede demostrar que algunos programas son correctos. No es fácil, pero se puede hacer. Ese es el objetivo de la prueba del teorema formal (una parte de los métodos formales). Los teoremas de incompletitud de Gödel sí aparecen aquí: no se puede demostrar que todos los programas sean correctos. Eso no significa que sea completamente inútil usar métodos formales porque algunos programas pueden demostrarse formalmente que son correctos.

Nota: Los métodos formales impiden la posibilidad de que un rayo cósmico golpee el procesador y se ejecute en launch_missiles()lugar de hacerlo a+b. Analizan programas en el contexto de una máquina abstracta en lugar de máquinas reales que están sujetas a perturbaciones de un solo evento, como el rayo cósmico de Robert Harvey.

Aquí hay muchas buenas respuestas, pero todas parecen eludir el punto crítico, que es el siguiente: todos esos teoremas tienen una estructura similar y dicen cosas similares, y lo que dicen no es "probablemente sea imposible escribir correctamente programas "(para algún valor específico de" correcto "y" programa "que varía en cada caso), pero lo que hacen decir es que 'es imposible evitar que alguien escribe un programa incorrecto que no podemos probar que es incorrecta' ( etc)

Tomando el ejemplo específico del problema de detención, la diferencia se vuelve más clara: obviamente, hay programas que probablemente se detengan, y otros programas que probablemente nunca se detengan. Que haya una tercera clase de programas cuyo comportamiento no pueda determinarse de ninguna manera no es un problema si todo lo que queremos hacer es escribir un programa que se pueda detener, ya que simplemente podemos evitar escribir un programa que pertenezca a esa clase.

Lo mismo es cierto con el teorema de Rice. Sí, para cualquier propiedad no trivial de un programa, podemos escribir un programa que no pueda tener esa propiedad probada como verdadera o falsa; También podemos evitar escribir dicho programa porque podemos determinar si un programa es demostrable.

Mi respuesta será desde la perspectiva de los negocios del mundo real y los desafíos que enfrenta cada equipo de desarrollo. Lo que veo en esta pregunta y muchas de las respuestas es realmente sobre el control de defectos.

El código puede estar libre de errores. Tome cualquiera de los ejemplos de código "Hello World" para cualquier lenguaje de programación y ejecútelo en la plataforma a la que está destinado y funcionará de manera consistente y producirá los resultados deseados. Allí termina cualquier teoría sobre la imposibilidad de que el código esté libre de errores.

Los posibles errores aparecen a medida que la lógica se vuelve más compleja. El simple ejemplo de Hello World no tiene lógica y hace lo mismo estático cada vez. Tan pronto como agregue un comportamiento dinámico impulsado por la lógica, es lo que introduce la complejidad que conduce a los errores. La lógica en sí misma puede ser defectuosa, o los datos que se ingresan a la lógica pueden variar de una manera que la lógica no maneja.

Una aplicación moderna también depende de las bibliotecas en tiempo de ejecución, CLR, middleware, bases de datos, etc. que, si bien ahorran tiempo de desarrollo en general, también son capas donde pueden existir errores dentro de esas capas y pasar desapercibidas a través del desarrollo y las pruebas UAT y en la producción.

Por último, la cadena de aplicaciones / sistemas de los que la aplicación consume datos que alimentan su lógica son todas fuentes de posibles errores, ya sea dentro de su lógica, o dentro de las pilas de software que se encuentran en la parte superior, o los sistemas ascendentes que consume datos.

Los desarrolladores no tienen el control del 100% de cada pieza móvil que admite la lógica de su aplicación. En realidad, no tenemos mucho control. Es por eso que las pruebas unitarias son importantes, y la configuración y la gestión de cambios son procesos importantes que no debemos ignorar o ser flojos / descuidados.

Además, los acuerdos documentados entre su aplicación que consumen datos de una fuente más allá de su control, que define el formato específico y las especificaciones para los datos transferidos, así como cualquier límite o restricción que su sistema asume que el sistema fuente es responsable de garantizar que la salida esté dentro esos límites

En la aplicación del mundo real de la ingeniería de software, no podrá hacerlo volar explicando a la empresa por qué, en teoría, las aplicaciones no pueden estar libres de errores. Las discusiones de esta naturaleza entre la tecnología y el negocio nunca sucederán, excepto después de un mal funcionamiento tecnológico que afectó la capacidad del negocio para ganar dinero, evitar perder dinero y / o mantener con vida a las personas. La respuesta a "cómo puede suceder esto" no puede ser "déjenme explicar esta teoría para que entiendan".

En términos de cálculos masivos que teóricamente podrían llevar una eternidad realizar el cálculo y obtener un resultado, una aplicación que no puede finalizar y regresar con un resultado, eso es un error. Si la naturaleza del cómputo es tal que consume mucho tiempo y es intensivo en cómputo, usted toma esa solicitud y le brinda retroalimentación al usuario sobre cómo / cuándo puede recuperar el resultado, y comienza los hilos paralelos para obtenerlo. Si esto tiene que suceder más rápido de lo que se puede hacer en un servidor, y es un negocio lo suficientemente importante, entonces puede escalarlo en tantos sistemas como sea necesario. Esta es la razón por la cual la nube es muy atractiva, y la capacidad de activar nodos para asumir el trabajo y reducirlos cuando haya terminado.

Si existe la posibilidad de obtener una solicitud que ninguna cantidad de potencia de cómputo puede completar, no debe pasar el tiempo corriendo hasta el infinito con un proceso de negocios esperando la respuesta a lo que la empresa cree que es un problema finito.

No creo que el código esté 100% libre de errores porque el código nunca está realmente terminado. Siempre puedes mejorar lo que escribes.

La programación es un campo de la ciencia y las matemáticas, en cuyo caso ambos son infinitos. Lo mejor de ser desarrollador es que nuestro trabajo es interminable.

Hay más de mil formas de escribir una sola línea de código. La idea es escribir la versión más optimizada de esa línea de código, pero puede que no esté libre de errores. Sin errores se refiere a la idea de que su código es indescifrable y que todo el código puede romperse en algún grado o método.

Entonces, ¿puede el código ser eficiente? Si.
¿Se puede optimizar el código sin cesar? Si.
¿Puede el código estar libre de errores? No, simplemente no has encontrado una manera de romperlo todavía.
Dicho esto, si se esfuerza por mejorar usted mismo y sus prácticas de escritura de códigos, será difícil romper su código.