¿Hay algunas lenguas del mundo real demostrables? (Scala?)

StackOverflow https://stackoverflow.com/questions/4065001

Pregunta

Me enseñaron acerca de los sistemas formales en la universidad, pero me ha decepcionado la forma en que no lo hicieron parecen ser utilizados en el mundo real.

Me gusta la idea de ser capaz de saber que algo de código (objeto, función, lo que sea) funciona, no por las pruebas, sino por prueba .

Estoy seguro de que todos estamos familiarizados con los paralelos que no existen entre la ingeniería física e ingeniería de software (se comporta de acero como era previsible, el software puede hacer nada - quien sabe), y me gustaría saber si hay las lenguas que se pueden utilizar en el mundo real (está pidiendo un framework de desarrollo web es mucho pedir?)

He oído cosas interesantes acerca de la capacidad de prueba de los lenguajes funcionales como la Scala.

A medida que el software ingenieros ¿Qué opciones tenemos?

¿Fue útil?

Solución

Sí, hay lenguajes diseñados para escribir software demostrablemente correcta. Algunos incluso se utilizan en la industria. Spark Ada es probablemente el ejemplo más destacado. He hablado con algunas personas en Praxis Sistemas Críticos limitada que la utilizaron para el código que se ejecuta en Boings (para el control del motor) y parece bastante agradable. (Aquí hay una gran resumen / descripción de la lengua .) Este sistema de prueba que acompaña idioma y utiliza la segunda técnica descrita a continuación. Ni siquiera se admite la asignación de memoria dinámica!

Mi impresión y la experiencia es que hay dos técnicas para la escritura de software correcto:

  • Técnica 1: Escribir el software en un idioma que se sienta cómodo con (C, C ++ o Java por ejemplo). Tome una especificación formal de este tipo de lenguaje, y demostrar que su programa correcto.

    Si su ambición es ser 100% correcto (que es lo más a menudo un requisito en la industria del automóvil / aeroespacial) que estaría gastando poco tiempo de programación, y más proving tiempo.

  • Técnica 2: escribir el software en un lenguaje un poco más incómoda (algún subconjunto de Ada o versión modificada de OCaml por ejemplo) y escribir la prueba corrección a lo largo del camino. Aquí la programación y prueba va de la mano. Programación en Coq incluso les equipara completamente! (Consulte la Curry-Howard correspondencia )

    En estos escenarios que va siempre terminan con un programa correcto. (Se garantizará que un fallo está enraizado en la especificación.) Usted será probable que pasar más tiempo en la programación, sino por el contrario estás demostrando que corregir en el camino.

Tenga en cuenta que ambos enfoques bisagras en el hecho de que tiene una especificación formal a la mano (¿cómo más se puede decir lo que es la conducta correcta / incorrecta), y una semántica formalmente definidas de la lengua (qué otra manera sería usted capaz de decir lo el comportamiento real de su programa es).

Aquí hay algunos ejemplos más de los enfoques formales. Si se trata de "mundo real" o no, depende de a quién le pregunte: -)

No conozco un solo idioma aplicación web "demostrablemente correcta" UR . A Ur-programa que "pasa por el compilador" no se garantiza que:

  • sufre de cualquier tipo de ataques de inyección de código
  • Vuelta inválida HTML
  • contener enlaces intra-uso en la aplicación
  • Tiene desajustes entre los formularios HTML y los campos esperados por sus manejadores
  • Incluya código del lado del cliente que hace suposiciones incorrectas sobre la "AJAX" servicios al estilo que el servidor web remoto proporciona
  • Intento no válido de SQL consultas
  • Uso indebido o cálculo de referencias unmarshaling en comunicación con bases de datos SQL o entre navegadores y servidores web

Otros consejos

Con el fin de responder a esta pregunta, que realmente necesita para definir lo que entendemos por "demostrable". Como Ricky señaló, cualquier idioma con un sistema de tipos es una lengua con un sistema integrado de prueba que se ejecuta cada vez que se compila el programa. Estos sistemas de prueba son casi siempre tristemente impotente - contestar preguntas como String vs Int y evitar preguntas como "es la lista ordenada?" - pero son sistemas a prueba de ninguno de los de menos

.

Por desgracia, el más sofisticado sus objetivos de prueba, más difícil es trabajar con un sistema que pueda revisar sus pruebas. Esto aumenta muy rápidamente en indecidibilidad si tenemos en cuenta el gran tamaño de la clase de problemas que son indecidible en las máquinas de Turing. Claro, que teóricamente puede hacer cosas básicas como la prueba de la exactitud de su algoritmo de ordenación, pero nada más que eso va a ser pisando sobre hielo muy delgado.

A pesar de demostrar algo tan simple como la corrección de un algoritmo de ordenación requiere un sistema de prueba relativamente sofisticada. (Nota: puesto que ya hemos establecido que los sistemas de tipo son un sistema de prueba integrada en el lenguaje, voy a hablar de las cosas en términos de la teoría de tipos, en lugar de agitar mis manos aún con más fuerza) Estoy bastante seguro de que una plena prueba de la corrección en la lista de clasificación requeriría alguna forma de tipos dependientes, de lo contrario no tiene manera de hacer referencia a los valores relativos en el nivel de tipo. Este se inicia inmediatamente irrumpir en ámbitos de la teoría de tipos que han demostrado ser indecidible. Así, mientras que usted puede ser capaz de demostrar la corrección en su lista algoritmo de ordenación, la única manera de hacerlo sería utilizar un sistema que también permitirá expresar pruebas que no se puede verificar. En lo personal, me parece muy desconcertante.

Hay también el aspecto facilidad de uso que he aludido anteriormente. Cuanto más sofisticado sea el sistema tipo, el menos agradable que es usar. Eso no es una regla dura y rápida, pero yo creo que es cierto para la mayor parte. Y como con cualquier sistema formal, que a menudo se encuentra que expresa la prueba es más trabajo (y más propenso a errores) que la creación de la aplicación en el primer lugar.

Con todo lo que fuera del camino, vale la pena señalar que el sistema de tipos de Scala (como Haskell) es Turing completo, lo que significa que puede teóricamente utilizarla para probar cualquier propiedad decidable acerca de su código, siempre que haya escrito el código de tal manera que es susceptible a este tipo de pruebas. Haskell es casi seguro que una lengua mejor para ello que Java (ya que la programación a nivel de tipo de Haskell es similar a Prolog, mientras que la programación a nivel de tipo de Scala es más similar a SML). No aconsejo que utilice sistemas de tipo de Scala o Haskell de esta manera (pruebas formales de corrección algorítmica), pero la opción es teóricamente disponible.

En conjunto, creo que la razón por la que no ha visto los sistemas formales en el "mundo real" se deriva del hecho de que los sistemas de prueba formal han cedido a la tiranía implacable del pragmatismo. Como ya he mencionado, hay mucho esfuerzo involucrado en la elaboración de sus pruebas de corrección que es casi nunca vale la pena. La industria decidió hace mucho tiempo que era más fácil para crear pruebas ad hoc de lo que era para ir a través de cualquier tipo de proceso de razonamiento formal analítica.

lenguajes de tipo demuestran la ausencia de ciertas categorías de culpa. El más avanzado es el sistema de tipos, los más fallos que puedan demostrar la ausencia de.

Para la prueba de que funciona un programa entero, sí, usted está caminando fuera de los límites de los lenguajes ordinarios, en los que las matemáticas y la programación se encuentran entre sí, se dan la mano y luego proceden a hablar utilizando símbolos griegos acerca de cómo los programadores no pueden manejar griega símbolos. Eso es alrededor de la S de todas formas.

Usted está haciendo una pregunta que muchos de nosotros han pedido a lo largo de los años. No sé que tengo una buena respuesta, pero aquí hay algunas piezas:

  • Hay lenguas bien entendido con la posibilidad de ser probada en uso hoy en día; Lisp través ACL2 es uno, y por supuesto el Esquema tiene una bien entendido definición formal también.

  • una serie de sistemas han tratado de utilizar lenguajes funcionales puros, o los casi puros, como Haskell. Hay un buen número de métodos de trabajo formal en Haskell.

  • Volviendo más de 20 años, había una cosa efímera para el uso de mano a prueba de un lenguaje formal que luego fue traducido rigurosamente en un lenguaje compilado. Algunos ejemplos eran de IBM Software para salas blancas, ACL, gitana, y se levantó de la Lógica Computacional, John McHugh y mi trabajo en la compilación fidedigna de C, y mi propio trabajo a la mano a prueba los sistemas de programación C. Todos ellos dieron un poco de atención, pero ninguno de ellos lo hizo mucho en la práctica.

Una pregunta interesante, creo, es lo que las condiciones suficientes para conseguir ser los enfoques formales en la práctica? Me encantaría escuchar algunas sugerencias.

Se puede investigar lenguajes puramente funcionales como Haskell, que se utiliza cuando uno de sus requisitos es demostrabilidad .

Este es un divertido leer si usted está interesado acerca de los lenguajes de programación funcionales y pura lenguajes de programación funcional.

usos reales de dichas lenguas demostrables sería muy difícil de escribir y entender afterwoods. el mundo de los negocios necesidades de software de trabajo, rápido.

idiomas "demostrables" simplemente no haga escala para la escritura / lectura de código base de un gran proyecto y sólo parece funcionar en los casos pequeñas y aisladas de uso.

Estoy involucrado en dos idiomas demostrables. El primero es el lenguaje soportado por Perfect desarrollador, un sistema para especificar sotfware, refinarlo y la generación de código. Ha sido utilizado en algunos sistemas grandes, incluyendo PD sí mismo, y se enseña en varias universidades. El segundo idioma demostrable que estoy involucrado con comprobable es un subconjunto de Misra-C, ver C / C ++ Verificación Blog de más.

Omega .

introducción contiene una implementación relativamente indolora de AVL con árboles incluida la prueba corrección.

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

EDITAR ===== Eliminado mis ideas incorrectas sobre ML ser "demostrable".

Mi (polémica) definición de "mundo real" en el contexto del código demostrablemente-correcta es:

  • Debe implicar cierto grado de Automatización , de lo contrario vas a pasar demasiado grande prueba del tiempo y se trata de pequeños detalles desordenados, y va a ser totalmente impracticable (excepto tal vez para el control de la nave espacial software y ese tipo de cosas, por lo que en realidad se podría querer pasar Megabucks en controles minuciosos).
  • Se debe admitir un cierto grado de programación funcional , que le ayuda a escribir código que es muy modular, reutilizable y fácil de razonar acerca. Obviamente, no es necesaria la programación funcional para escribir o demostrando Hello World, o una variedad de programas sencillos, pero en un momento dado, la programación funcional llega a ser muy útil.
  • Si bien no necesariamente tiene que ser capaz de escribir el código en un lenguaje de programación convencional, como alternativa, al menos debe ser capaz de máquina-traductor de código en el código razonablemente eficiente escrito en un lenguaje de programación convencional, de una manera fiable.

Los anteriores son requisitos relativamente más universales. Otros, como la capacidad de modelar código imperativo, o la capacidad para probar las funciones de orden superior correcta, puede ser importante o esencial para algunas tareas, pero no todos.

A la vista de estos puntos, muchos de los instrumentos enumerados en el esta entrada del blog mío puede ser útil - aunque son casi todos, ya sea nueva y experimental, o desconocido para la gran mayoría de los programadores de la industria. No existen algunas herramientas muy maduro cubiertos sin embargo.

¿Qué hay de Idris y Agda ? Bastante real mundo?

Como un buen ejemplo de la vida real, no es un proyecto que pretende ofrecer un verificó librería HTTP REST escrito en Agda, llamado Lemmachine: https://github.com/larrytheliquid/Lemmachine

Licenciado bajo: CC-BY-SA con atribución
No afiliado a StackOverflow
scroll top