¿Es lógico / matemáticamente posible demostrar que el código libre de errores no existe?

En ningún momento

• No es suficiente que el programa se comporte perfectamente en circunstancias normales; un programa sin errores tendría que comportarse perfectamente, o al menos con sensatez, en circunstancias normales, por el mal uso del usuario, incluido el hardware necesario faltante (por ejemplo, una aplicación de grabación de discos debería responder razonablemente a la falta de una grabadora) camino a los intentos activos de rotura maliciosa.
• Incluso el programa más simple que cumpla con sus requisitos probablemente tendrá muchas formas en que circunstancias imprevistas podrían romperlo. El ejemplo de “Hola mundo” de Rob Rix es bueno, lo que ya he explorado más profundamente: Hola Mundo, corta cuatro maneras
• No se pueden descartar circunstancias imprevistas: los usuarios encontrarán formas nuevas e ingeniosas de usar su programa de manera incorrecta, y los atacantes encontrarán formas nuevas e inventivas para explotar sus fallas. O no consideró tales casos (en una o ambas categorías) o no los consideró en todos.
• Hacer que el programa sea más robusto — anticipando y manejando más variedad de circunstancias — agrega complejidad; cualquier complejidad es un buen lugar para que un insecto aceche.
• Si va en la dirección opuesta, y elimina todo el código fuente , entonces tiene un programa sin ningún código defectuoso, pero no hace lo que estaba destinado a hacer *, por lo que claramente no funciona, ¿verdad?

De estas observaciones podemos concluir que no existe un programa de software que cumpla con sus requisitos y que no contenga absolutamente ningún error.

—-

* Suponiendo que el objetivo no era “no hacer nada”, para el cual un programa vacío es válido y correcto en algunos idiomas. Pero entonces, la mayoría de esos idiomas tienen intérpretes o tiempos de ejecución …

Se trata de las definiciones.

Hay muchos niveles en los que puede tener “errores”, y muchos de ellos tienen más que ver con las debilidades de los lenguajes humanos que con los programas informáticos mal codificados.

En última instancia, el problema radica en la simple idea de que no se puede simular completamente el universo, y como un lenguaje de especificación describe una simulación del problema que se especifica, ningún lenguaje de especificación, ya sea un lenguaje de computadora o un lenguaje humano, puede capturar completamente todo posibles requisitos deseados e interacciones entre los requisitos de todos los posibles problemas.

Sin embargo, si asume que puede indicar perfectamente los requisitos, ya ha demostrado que existe una “solución libre de errores”, ya que el programa de computadora debería ser una simple reasignación del lenguaje de requisitos al lenguaje de implementación. (al menos para problemas decidibles: hay problemas que pueden establecerse con precisión y que no pueden ser decididos por una computadora con máquina de Turing)

Los “errores” son esencialmente fallas en la reasignación o traducción entre estos idiomas. Pero si el lenguaje de requisitos es en sí mismo un lenguaje de computadora, la reasignación es nula y usted ha hecho su “prueba”.

Dicho esto, en la vida real, es muy difícil establecer los requisitos para un problema no trivial y, a medida que el problema evoluciona, los requisitos evolucionan. Mantener el código que implementa los requisitos actualizados con los requisitos en evolución es una fuente de errores (y uno particularmente desagradable), y es en muchos aspectos estos errores a menudo son más difíciles de identificar y “arreglar” que los errores debidos a la simple codificación errónea de requisitos que de otra manera se entenderían bien.

Intentemos formular su declaración correctamente. Necesitamos algunos conocimientos previos antes.

1. Todos los algoritmos existentes se pueden describir en términos de la máquina de Turing.
2. Dado un programa para la máquina de Turing y el estado inicial de la cinta, no existe un algoritmo determinista que pueda determinar si la máquina de Turing se detiene o no en un tiempo finito. Ver problema de detención.

Del mismo modo, no existe un algoritmo determinista para descubrir que la implementación de un algoritmo esté libre de errores. Esto no significa que no pueda verificar la implementación de un algoritmo en particular y demostrar que está libre de errores. No hay (y nunca habrá) un algoritmo general para hacerlo.

Ofrecería para el análisis un programa de sistema muy antiguo de la era IBM OS / 360 (1970 más o menos): IEFBR14.

IEFBR14 fue un programa que consistía en una sola línea:

BR14

En C, el programa sería similar a

principal(){}

“BR14” es una declaración de “devolución”.

Sí, el programa no hizo nada excepto regresar al sistema operativo. Su propósito era permitir al usuario realizar actividades del sistema como crear o eliminar objetos. Diría “ejecutar IEFBR14 utilizando el archivo X y eliminar X al final”. En esencia, el sistema operativo ejecutaría el programa (sin hacer nada) y luego eliminaría el archivo. Sí, esto se convirtió en “eliminar X”.

Sin embargo, todo el sistema de archivos y otros efectos secundarios tuvieron lugar fuera de IEFBR14. Desde el punto de vista de la verificación formal, IEFBR14 no tenía condiciones previas (aparte del registro 14 que contenía una dirección de retorno) ni condiciones posteriores. Y satisfizo todo esto.

Desde la perspectiva de “simplemente programemos esto y lo depuremos hasta que sea bueno”, como otros han dicho, nunca. Como solía decir Gilda Radner en Saturday Night Live, “Siempre es algo …” Siempre hay otro caso que no has pensado probar.

Sin embargo, hay todo un campo de investigación de Corrección (informática), que adopta una variedad de enfoques. Si su clase introductoria le hizo escribir condiciones previas y condiciones posteriores para su código, ese es el primer paso en ese camino (una versión informal del triple de Hoare), pero hay un agujero de conejo que es bastante profundo. Hay idiomas enteros y ramas de las matemáticas dedicadas a hacerlo posible, y no hace mucho tiempo que el Departamento de Defensa contrataría a docenas de doctores para revisar el código crítico utilizando estos métodos, como entiendo por amigos contratistas de defensa.

Por supuesto, puedes ver el problema. Para probar que el programa es correcto, debe convertir tanto la especificación como el programa a una nueva forma abstracta, y confiar en el análisis de los seres humanos, que son todos procesos propensos a errores. Está escribiendo el programa tres veces (formalización de las especificaciones, el programa real y el modelo del programa), y comparar dos de ellos para probar un tercero no tendrá problemas.

También alegremente (como un niño o un abogado) ignora el mal comportamiento si no se requiere que sea bueno.

Sin embargo, si no toca el código, la confianza de que no haya un error va asintóticamente hacia cero, cuanto más tiempo esté en uso el código. Nunca será cero, pero si ha estado utilizando un programa durante una década o dos y nunca ha visto un problema, es cada vez más probable que nunca lo vea.

Hay un tema completo dedicado a probar la corrección del software.

Debido al problema de detención, es imposible examinar un programa arbitrario para saber si tiene un error, por lo que ese enfoque no se utiliza.

En cambio, cada segmento de código tiene aserciones asociadas. Hay aserciones al principio que se supone que se mantienen antes de que se ejecute el código, y aserciones al final que se supone que se mantienen después de que se ejecuta el código. El segmento está hecho de subsegmentos con sus propias aserciones asociadas. Si puede probar a partir de la suposición del segmento y las afirmaciones de los subsegmentos que contiene la conclusión, entonces ese segmento es correcto. Si hace esto para todos los segmentos en el código, entonces es correcto.

Corrección (informática)
Verificación formal
Página en ucsc.edu

No, porque es posible un código libre de errores (excluyendo posibles fallas relacionadas con el hardware)

1. Tome un método base libre de errores (por ejemplo, como una función vacía)
2. Siempre hay algo posible para agregar a este código sin agregar un error

Solo hay una cosa segura en este universo, la incertidumbre.

en lugar de eso, pregúntese qué tan seguro está de que su software funcionará para sus usuarios. El 80% de los usuarios utilizará el 20% de sus funciones, las identificará e intentará cubrir los escenarios máximos para ellas.

Es un hecho, en el mundo del programador, que es imposible escribir código 100% libre de errores.

He estado programando desde 1965 y eso no es un hecho en mi mundo. Lo cierto es que cada vez es menos probable que el código esté libre de errores a medida que aumenta la complejidad, y que el umbral es bastante bajo, pero no es que sea imposible . De hecho, hay pequeños sistemas que probablemente no tengan errores.

¿Pero es humanamente imposible escribir código libre de errores?

En la medida en que sea “imposible”, eso se debe a la acumulación de errores humanos.

¿o podemos demostrar matemáticamente que un código no trivial nunca puede estar 100% libre de errores?

No, no podemos Tenga en cuenta que es posible tener programas informáticos que utilicen algoritmos genéticos para desarrollar otros programas informáticos que cumplan con las especificaciones formales. No existe un límite teórico sobre la complejidad de las especificaciones a las que los programas generados se ajustan y, por lo tanto, están libres de errores. Actualmente no desarrollamos software de esta manera porque no es computacionalmente factible, pero eso podría cambiar.

El error nunca está en el código, está en el cerebro. Entonces, el software libre de errores necesita un cerebro libre de errores. Entonces, básicamente depende del individuo.

Absolutamente ninguna relación con la programación o la codificación en absoluto.

¡Espero que no! Porque entonces, las matemáticas serían inconsistentes. ¡Existe un código libre de errores! Por ejemplo, un programa con especificación indefinida está libre de errores (no importa lo que haga el programa, satisface la especificación).

Incluso tenemos algunos programas libres de errores no triviales, como el microkernel L4 o algunos procesadores canalizados.

No, la premisa de esta pregunta es incorrecta.

De hecho, es posible producir código libre de errores. Este proceso se llama verificación formal:

Verificación formal – Wikipedia

Desafortunadamente, es muy costoso en cuanto a costo / tiempo, por lo que nadie lo hace, excepto en la academia.

Su programa de ejemplo en la pregunta tiene un error. La cadena debe terminar con “\ n”:

$ g ++ test.cpp
$ ./a.out
hola mundo $

Sólo digo.

No.

Es posible escribir código libre de errores. Sin embargo, es extremadamente improbable ya que el programa crece en tamaño.

Y, dado que su código probablemente depende de compiladores preexistentes, bibliotecas, hardware, etc., es probable que haya algún problema en alguna de ellas. Eso significa que incluso si su código está “libre de errores”, el programa podría fallar algunas veces.

No, no es un hecho.

Es posible escribir código libre de errores, pero simplemente no es práctico para ningún proyecto no trivial.

Tuvimos un maestro que nos enseñó algunas cosas:
– Si escribes un programa ideal de “Hola mundo”, ya tienes un error allí.
– Si arreglaste un error, hiciste al menos uno más.

Eso fue en las primeras clases de programación (si no la primera).
Ahora todos estamos libres de preguntas sobre el código “sin errores”. : +]

Decir “codificar” sin “error” es como decir “hacer algo” sin “riesgo”.

La única forma de evitar el riesgo es no hacer “ese algo” / “codificación”.

Pero, al menos, podemos evitar todos los errores previsibles. No olvide agregarle la palabra “punto”. 🙂

No existe el software libre de errores.

Cada vez que un programa actúa inesperadamente, o cada vez que alguien no sabe qué hacer, es un error.

Los más inteligentes se darán cuenta de que la palabra “error” en este caso depende completamente de qué tipo de persona es el usuario. Y así es como debe ser.