Programación de enseñanza y métodos formales

Question

Aquí hay una especie de pregunta extraña. Estoy en el proceso de escribir un libro sobre cómo aprender a programar usando métodos formales, y lo enfocaré hacia personas con alguna experiencia en programación. La idea es enseñarles a ser programadores de alta calidad.

La notación básica va a ser de Dijkstra's Discipline of Programming, junto con algunas extensiones de concurrencia y comunicaciones.

A diferencia de EWD, quiero que mis alumnos escriban programas ejecutables reales. Eso significa en algún momento traducir la notación EWD a algún otro idioma. Cuando comencé a hacer programación formal apunté a C, pero terminaste escribiendo muchas plomería, además de todas las complejidades del tratamiento de punteros, etc. Ruby es un objetivo obvio posible, como lo es Scheme o Lisp. Pero también hay varios lenguajes de funciones; ya que estoy especialmente interesado en la concurrencia, Erlang parece una posibilidad.

Así que, finalmente, aquí está mi pregunta: ¿Qué idioma (s) debo enseñar a mis lectores a enfocar sus programas formalmente desarrollados?

Answer 1

Charlie,

siempre he asociado la obra maestra de Dijkstra con un modelo de programación en el que el centro del escenario es ocupado por los bucles y matrices. Si te estás quedando cerca de Dijkstra (por ejemplo, computando las precondiciones más débiles), creo que encontrarás que los lenguajes funcionales no encajan demasiado bien. De los lenguajes populares que proporcionan un buen soporte para la programación imperativa con bucles y matrices, quizás Python lleva el menor equipaje adicional.

Esto no quiere decir que los lenguajes funcionales sean inadecuados para los métodos formales --- son muy adecuados --- pero el estilo es bastante diferente de Dijkstra. Los métodos preferidos enfatizan las pruebas de cálculo; vea el trabajo de Richard Bird sobre cómo resolver el Sudoku (que es pesado) o el libro de texto de Richard Bird y Phil Wadler.

Para concurrencia, depende mucho del modelo de simultaneidad (y de los métodos formales) en los que cree. El ML Concurrente de John Reppy es un bello modelo de transmisión de mensajes. Erlang también tiene un buen modelo restrictivo limpio. Por otro lado, la programación con bloqueos y secciones críticas es tan difícil, puede haber más beneficios para los métodos formales en esa situación. otros

dos observaciones de paso, que puede ser de interés para su investigación de fondo:

• El único programador que he conocido, que aplica métodos de Dijkstra en la práctica a los sistemas reales fue Greg Nelson, que estaba trabajando en moduladores 3. (Greg y Mark Manasse escribieron juntos el sistema de ventana Trestle.) Modula-3 era un lenguaje muy agradable que Digital permitía morir por imprudencia e incompetencia. Greg tenía un buen artículo de TOPLAS sobre una extensión del cálculo de Dijkstra.

• El lenguaje de modelado de Gerard Holzmann SPIN se basa directamente en el lenguaje de comandos guardados de Dijkstra, y también admite concurrencia. Su propósito es el control de modelos, no la programación, y hay algunas idiosincrasias, pero existe una fuerte conexión con los métodos formales, y es realmente genial poder modelar tus afirmaciones. Cualquier persona interesada en métodos formales querrá verificarlo.

(Editar:. Aquí hay un enlace al documento Greg Nelson, o uno de ellos - CRM)

Answer 2

Esa es una buena idea. Creo que Scheme es una buena opción, ya que permite poner en práctica (en forma de librerías) diferentes abstracciones con mínimos esenciales. También es fácil de traducir del esquema de un sistema de verificación como PVS (http://pvs.csl.sri.com/)

aplausos

Answer 3

Crecí en Lisp y Scheme y amarlos a ambos. Creo que son excelentes idiomas para aprender de cero. Pero no estoy seguro de que alguien con experiencia en programación pueda acceder a esos idiomas. No obtendrás muchos éxitos en Amazon para tu libro con Scheme en el título. :)

C# es un lenguaje muy fácil de aprender y tiene todos los elementos básicos que necesitaría para profundizar en temas como la concurrencia con bastante rapidez. Tiene más aplicabilidad porque también puede orientar los conceptos OO y web. También es bastante popular y las empresas pagan por los libros de sus empleados, lo que siempre es bueno para las ventas ("Be a Kick Ass C# Programmer" va mucho más allá en una hoja de reembolso de gastos que "Concurrency in Modern Lisp").

F # es un lenguaje interesante. Tiene la belleza funcional de un Lisp o Scheme (bueno, no del todo, pero casi) y te da cierta habilidad para sumergirte en los temas de OOP, así como engancharte en .NET Framework para cosas de interfaz de usuario si quieres darle vida a las cosas. Pero, ahora mismo, es oscuro.

No puedo hablar con Ruby, así que personalmente, me gustaría morder la bala e ir con C#.

Answer 4

Creo que usted debería tener bastante experiencia en el lenguaje que usa para su libro, o alguien competente para revisar su código.

Personalmente, usaría Common Lisp, ya que estoy familiarizado con eso, y es un excelente lenguaje para implementar cualquier concepto. Otras opciones podrían ser Erlang, Haskell, Ruby o Python, quizás incluso algún dialecto ML. Soy parcial en contra de la familia C (incluyendo C# y Java), parecen estar atrapados en un nivel más bajo de pensamiento sobre conceptos.

Answer 5

Haciendo caso omiso de lo obvio ¿cuál es tu favoriteprogramminglanguage respuestas, puedo ver dos respuestas útiles:

Por un lado, que están tratando de demostrar métodos a lo que se supone que son los programadores intermedios.Si seleccionas un solo idioma y lo bendices como el idioma de tus libros, posiblemente alejarás a lectores potenciales que no prefieren ese idioma por una razón u otra. Dado que está demostrando métodos, tiene el lujo de utilizar fragmentos en idiomas que ilustran su punto de forma concisa. Por ejemplo, el único lenguaje disponible para demostrar RIIA es probablemente C++, pero este mismo lenguaje es bastante pobre para mostrar cómo realizar análisis de fuente. El esquema es ideal para el análisis de fuentes, pero no le ofrece muchas opciones para explorar los beneficios (y debilidades) de una tipificación fuerte. Usa muchos idiomas

Por otro lado, dado que usted está principalmente a la altura de los métodos de programación, no estoy totalmente seguro de que necesite un lenguaje real. Una notación bien definida es igual de buena y obliga a los lectores a centrarse en el punto que está haciendo en lugar de los detalles superficiales de un idioma u otro.

Answer 6

Honestamente, no puedo recomendar Rubí para esto. Cuando programo el día a día en mi mundo comercial, me gusta bastante, sin duda mucho más que C o Java.Pero su semántica está tan mal definida que no confío tanto como C, aunque puedo pasar varias horas discutiendo sobre un enunciado y consultando ese libro blanco mucho más grueso que reemplazó K & R, salgo al final bastante convencido de que si tengo un compilador conforme (sí, lo sé, soy un soñador, pero trabaje conmigo aquí) sé lo que está saliendo del otro lado.

Ruby es maravilloso en muchos aspectos, pero en lo que se refiere a lo formal, los dos nunca se encontrarán.

Tiendo a votar por Haskell yo mismo, porque cada vez que doy la vuelta me sorprende cuánto sentido tiene todo en la definición del lenguaje. (Aunque es cierto que después de solo un año más o menos, estoy seguro de que no he explorado la mitad de las esquinas de Haskell 98.)

Y también entiendo la función Dikjstra vs. funcional; volviendo atrás y reading his papers está muy en un mundo imperativo; No estoy calificado para decir si realmente fue por el camino equivocado allí. Tal vez me siento abrumado por lo bueno que es su escritura, tanto como su pensamiento. Pero pareció complacerlo, ¿qué tal usar Algol 60?

Answer 7

Existen bastantes universidades que usan Perfect Developer para enseñar métodos formales (descargo de responsabilidad: estoy conectado con este producto). Se basa en un lenguaje para expresar especificaciones, refinamiento de datos y algoritmos. Tiene un comprobador de teoremas automático para la verificación y un generador de código que puede producir C++, C# y Java. El diseño de PD estaba muy inspirado en "A Disciplina de programación", sin embargo, encontramos que la notación es poco práctica para sistemas grandes, por lo que la notación se ha distanciado un poco de la de Dijktra.