usar sirve settitle que para codigo java scala testing functional-programming formal-verification

java - sirve - ¿Hay algún lenguaje del mundo real que se pueda demostrar?(scala?)



settitle java (11)

Me enseñaron acerca de los sistemas formales en la universidad, pero me decepcionó que no parecieran usarse en la palabra real.

Me gusta la idea de poder saber que algún código (objeto, función, lo que sea) funciona, no por prueba, sino por prueba .

Estoy seguro de que todos estamos familiarizados con los paralelos que no existen entre la ingeniería física y la ingeniería de software (el acero se comporta de manera predecible, el software puede hacer cualquier cosa, ¡quién sabe!), Y me encantaría saber si hay algún lenguaje que puede usarse en la palabra real (¿es demasiado pedir un marco web?)

He escuchado cosas interesantes sobre la capacidad de prueba de lenguajes funcionales como Scala.

Como ingenieros de software , ¿qué opciones tenemos?

¿Qué hay de Idris y Agda ? ¿El mundo real es suficiente?

Como un buen ejemplo de la vida real, hay un proyecto que tiene como objetivo proporcionar una biblioteca HTTP REST verificada escrita en Agda, llamada Lemmachine: https://github.com/larrytheliquid/Lemmachine

Echa un vistazo a Omega .

Esta introduction contiene una implementación relativamente sencilla de los árboles AVL con la prueba de corrección incluida.

Estás haciendo una pregunta que muchos de nosotros hemos preguntado a lo largo de los años. No sé si tengo una buena respuesta, pero aquí hay algunas piezas:

  • Hay lenguajes bien entendidos con la posibilidad de ser probado actualmente; Lisp a través de ACL2 es uno, y por supuesto, Scheme también tiene una definición formal bien entendida.

  • varios sistemas han intentado usar lenguajes funcionales puros, o casi puros, como Haskell. Hay un poco de métodos formales que funcionan en Haskell.

  • Hace más de 20 años, hubo algo efímero en el uso de pruebas manuales de un lenguaje formal que luego se tradujo rigurosamente en un lenguaje compilado. Algunos ejemplos fueron Software Cleanroom de IBM, ACL, Gypsy y Rose de Computational Logic, John McHugh y mi trabajo sobre la compilación confiable de C, y mi propio trabajo sobre la prueba manual para la programación de sistemas C. Todos obtuvieron algo de atención, pero ninguno de ellos lo hizo mucho en la práctica.

Una pregunta interesante que hacer, creo, es ¿cuáles serían las condiciones suficientes para poner en práctica los enfoques formales? Me encantaría escuchar algunas sugerencias.

Estoy involucrado en dos idiomas demostrables. El primero es el lenguaje soportado por Perfect Developer, un sistema para especificar sotfware, refinarlo y generar código. Se ha utilizado para algunos sistemas grandes, incluida la PD, y se enseña en varias universidades. El segundo lenguaje demostrable en el que estoy involucrado es un subconjunto comprobable de MISRA-C; consulte el blog de verificación C / C ++ para obtener más información.

Los idiomas escritos prueban la ausencia de ciertas categorías de fallas. Cuanto más avanzado es el sistema de tipo, más fallas pueden demostrar la ausencia de.

Como prueba de que todo un programa funciona, sí, estás saliendo de los límites de los lenguajes comunes, donde las matemáticas y la programación se encuentran, dan la mano y luego hablan usando símbolos griegos sobre cómo los programadores no pueden manejar los símbolos griegos. Eso es sobre el Σ de todos modos.

Mi (polémica) definición de "mundo real" en el contexto del código que se puede probar de manera correcta es:

  • Debe involucrar cierto grado de automatización , de lo contrario, vas a pasar demasiado tiempo probando y lidiando con pequeños detalles desordenados, y va a ser totalmente impráctico (excepto tal vez para el software de control de naves espaciales y ese tipo de cosas, para lo cual en realidad podría querer gastar megabucks en cheques meticulosos).
  • Debe admitir un cierto grado de programación funcional , que le ayuda a escribir código que es muy modular, reutilizable y más fácil de razonar. Obviamente, la programación funcional no es necesaria para escribir o probar Hello World, o una variedad de programas simples, pero en cierto punto, la programación funcional se vuelve muy útil.
  • Si bien no necesariamente tiene que poder escribir su código en un lenguaje de programación convencional, como alternativa, al menos debería ser capaz de traducir a máquina su código en un código razonablemente eficiente escrito en un lenguaje de programación convencional, de manera confiable. camino.

Lo anterior son requisitos relativamente más universales. Otros, como la capacidad de modelar código imperativo o la capacidad de demostrar que las funciones de orden superior son correctas, pueden ser importantes o esenciales para algunas tareas, pero no para todas.

En vista de estos puntos, muchas de las herramientas enumeradas en esta publicación de mi blog pueden ser útiles, aunque casi todas son nuevas y experimentales, o desconocidas para la gran mayoría de los programadores de la industria. Sin embargo, hay algunas herramientas muy maduras cubiertas.

Puede investigar lenguajes puramente funcionales como Haskell, que se utilizan cuando uno de sus requisitos es comprobable .

This es una lectura divertida si le interesan los lenguajes de programación funcionales y los lenguajes de programación funcionales puros.

Sí, hay idiomas diseñados para escribir software que se pueda corregir. Algunos incluso se usan en la industria. Spark Ada es probablemente el ejemplo más destacado. He hablado con algunas personas de Praxis Critical Systems Limited que lo usaron para el código que se ejecuta en Boings (para el control del motor) y parece bastante agradable. (Aquí hay un gran resumen / descripción del idioma .) Este lenguaje y el sistema de prueba que lo acompaña utilizan la segunda técnica que se describe a continuación. ¡Ni siquiera es compatible con la asignación de memoria dinámica!

Mi impresión y experiencia es que hay dos técnicas para escribir el software correcto:

  • Técnica 1: escriba el software en un idioma que le resulte cómodo (C, C ++ o Java, por ejemplo). Tome una especificación formal de dicho lenguaje y demuestre que su programa es correcto.

    Si su ambición es ser 100% correcto (lo que con frecuencia es un requisito en la industria aeroespacial / automovilística), estaría pasando poco tiempo programando, y probando más tiempo.

  • Técnica 2: escriba el software en un lenguaje un poco más torpe (por ejemplo, un subconjunto de Ada o una versión modificada de OCaml) y escriba la prueba de corrección en el camino. Aquí la programación y la prueba van de la mano. ¡La programación en Coq incluso los equipa por completo! (Ver la correspondencia de Curry-Howard )

    En estos escenarios, siempre terminará con un programa correcto. (Se garantizará que un error esté arraigado en la especificación). Es probable que dedique más tiempo a la programación pero, por otro lado, está demostrando que es correcto en el camino.

Tenga en cuenta que ambos enfoques dependen del hecho de que tenga a mano una especificación formal (¿cómo podría saber qué es el comportamiento correcto / incorrecto) y una semántica del lenguaje formalmente definida (de qué otra manera sería capaz de decir cuál es el comportamiento real? de tu programa es).

Aquí hay algunos ejemplos más de enfoques formales. Si es "real" o no, depende de a quién le preguntes :-)

Solo conozco un lenguaje de aplicación web "probadamente correcto": UR . Un programa de Ur que "atraviesa el compilador" tiene la garantía de no:

  • Sufre de cualquier tipo de ataque de inyección de código
  • Devuelve HTML no válido
  • Contiene enlaces muertos dentro de la aplicación
  • Tener desajustes entre formularios HTML y los campos esperados por sus controladores
  • Incluya el código del lado del cliente que hace suposiciones incorrectas sobre los servicios de estilo "AJAX" que proporciona el servidor web remoto
  • Intente consultas SQL no válidas
  • Usar referencias o bases de datos impropias en la comunicación con bases de datos SQL o entre navegadores y servidores web

Scala está destinado a ser "mundo real", por lo que no se ha hecho ningún esfuerzo para hacerlo demostrable. Lo que puedes hacer en Scala es producir un código funcional. El código funcional es mucho más fácil de probar, lo que en mi humilde opinión es un buen compromiso entre el "mundo real" y la capacidad de prueba.

EDIT ===== Eliminé mis ideas incorrectas sobre que ML es "comprobable".

los usos del mundo real de tales lenguajes demostrables serían increíblemente difíciles de escribir y entender después de las maderas. el mundo de los negocios necesita un software en funcionamiento, rápido.

Los lenguajes "comprobables" simplemente no escalan para escribir / leer la base de código de un proyecto grande y solo parecen funcionar en casos de uso pequeños y aislados.

Para responder a esta pregunta, realmente necesitas definir lo que quieres decir con "comprobable". Como señaló Ricky, cualquier lenguaje con un sistema de tipos es un lenguaje con un sistema de prueba incorporado que se ejecuta cada vez que compila su programa. Estos sistemas de prueba casi siempre son tristemente impotentes, respondiendo preguntas como String vs Int y evitando preguntas como "¿está ordenada la lista?" - pero son, sin embargo, sistemas de prueba.

Desafortunadamente, cuanto más sofisticados sean sus objetivos de prueba, más difícil será trabajar con un sistema que pueda verificar sus pruebas. Esto se incrementa bastante rápidamente hasta la indecidibilidad cuando se considera el tamaño de la clase de problemas que son indecidibles en las máquinas de Turing. Claro, teóricamente puedes hacer cosas básicas como probar la corrección de tu algoritmo de clasificación, pero nada más que eso va a pisar hielo muy delgado.

Incluso para probar algo simple como la corrección de un algoritmo de clasificación, se requiere un sistema de prueba comparativamente sofisticado. (nota: dado que ya hemos establecido que los sistemas de tipo son un sistema de prueba integrado en el lenguaje, voy a hablar de cosas en términos de teoría de tipos, en lugar de agitar las manos aún más vigorosamente) Estoy bastante seguro de que La corrección completa a prueba en la ordenación de listas requeriría algún tipo de tipos dependientes; de lo contrario, no tendría forma de hacer referencia a los valores relativos en el nivel de tipo. Esto inmediatamente comienza a romperse en los reinos de la teoría de tipos que han demostrado ser indecidibles. Por lo tanto, si bien es posible que demuestres la corrección de tu algoritmo de clasificación de listas, la única forma de hacerlo sería usar un sistema que también te permita expresar pruebas que no puede verificar. Personalmente, encuentro esto muy desconcertante.

También está el aspecto de facilidad de uso al que aludí anteriormente. Cuanto más sofisticado sea su sistema de tipos, menos agradable será su uso. Esa no es una regla difícil y rápida, pero creo que es cierto en su mayor parte. Y al igual que con cualquier sistema formal, a menudo encontrará que expresar la prueba es más trabajo (y más propenso a errores) que crear la implementación en primer lugar.

Con todo eso fuera del camino, vale la pena señalar que el sistema de tipos de Scala (como el de Haskell) es Turing Complete, lo que significa que teóricamente puedes usarlo para probar cualquier propiedad decidible sobre tu código, siempre que hayas escrito tu código en tal forma en que es susceptible a tales pruebas. Es casi seguro que Haskell es un lenguaje mejor para esto que Java (ya que la programación a nivel de tipo en Haskell es similar a Prolog, mientras que la programación a nivel de tipo en Scala es más similar a SML). No aconsejo que use los sistemas de tipos de Scala o Haskell de esta manera (pruebas formales de corrección algorítmica), pero la opción está teóricamente disponible.

En conjunto, creo que la razón por la que no has visto los sistemas formales en el "mundo real" proviene del hecho de que los sistemas formales de prueba han cedido a la implacable tiranía del pragmatismo. Como mencioné, hay mucho esfuerzo involucrado en crear sus pruebas de corrección que casi nunca vale la pena. La industria decidió hace mucho tiempo que era más fácil crear pruebas ad hoc que pasar por cualquier tipo de proceso analítico de razonamiento formal.