programming languages - Programación docente y métodos formales.
programming-languages dijkstra (7)
Charlie
Siempre he asociado la obra maestra de Dijkstra con un modelo de programación en el que el escenario central está ocupado por bucles y arreglos. Si se está pegando a Dijkstra (por ejemplo, calculando condiciones previas más débiles), creo que encontrará que los lenguajes funcionales no son una buena opción. De los lenguajes populares que brindan un buen soporte para la programación imperativa con loops y arreglos, quizás Python lleve el menor equipaje adicional.
Esto no quiere decir que los lenguajes funcionales sean inadecuados para los métodos formales (están muy bien adaptados), pero el estilo es muy diferente al de Dijkstra. Los métodos preferidos enfatizan las pruebas de cálculo; vea el artículo de Richard Bird sobre cómo resolver el Sudoku (que es un tema pesado) o el libro de texto de Richard Bird y Phil Wadler.
Para la concurrencia, depende mucho de qué modelo de concurrencia (y en qué métodos formales) crees. Concurrent ML de John Reppy es un hermoso modelo de paso 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 que puede haber más beneficios para los métodos formales en esa situación.
Otros dos comentarios que pueden ser de interés para su investigación de antecedentes:
El único programador que conocí que aplicó los métodos de Dijkstra en la práctica a sistemas reales fue Greg Nelson, que trabajaba en Modula-3. (Greg y Mark Manasse escribieron juntos el sistema de ventanas Trestle). Modula-3 fue un lenguaje muy agradable que Digital permitió que muriera a través de la inestabilidad y la incompetencia. Greg tenía un buen papel de TOPLAS en una extensión del cálculo de Dijkstra.
El lenguaje de modelado de Gerard Holzmann SPIN se basa directamente en el lenguaje de los comandos protegidos de Dijkstra, y también es compatible con la concurrencia. Su propósito es la verificación 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 sus afirmaciones. Cualquier persona interesada en métodos formales querrá comprobarlo.
(Editar: aquí hay un enlace al artículo de Greg Nelson , o uno de ellos. - CRM)
Aquí hay una especie de pregunta extraña. Estoy en el proceso de escribir un libro sobre aprender a programar utilizando métodos formales, y lo orientaré hacia personas con cierta experiencia en programación. La idea es enseñarles a ser programadores de alta calidad.
La notación básica será de Disciplina de programación de Dijkstra, junto con algunas extensiones de concurrencia y comunicaciones.
A diferencia de EWD, quiero que mis estudiantes eventualmente escriban programas ejecutables reales. Eso significa que en algún momento se traduce de la notación EWD a otro idioma. La primera vez que comencé a hacer programación formal apunté a C, pero terminas escribiendo mucha plomería, además, existen todas las complejidades de tratar punteros, etc. Ruby es un objetivo obvio, como Scheme o Lisp. Pero también hay varios lenguajes funcionales; Ya que estoy especialmente interesado en la concurrencia, Erlang parece una posibilidad.
Entonces, finalmente, aquí está mi pregunta: ¿Qué idioma (s) debo enseñar a mis lectores a orientar sus programas formalmente desarrollados?
Crecí en Lisp y Scheme y los amo a ambos. Creo que son excelentes idiomas para aprender desde cero. Pero, no estoy seguro de que alguien con alguna experiencia en programación llevara esos lenguajes. No vas a recibir muchos éxitos en Amazon por tu libro con Scheme en el título. :)
C # es un lenguaje muy fácil de aprender y tiene todos los conceptos básicos que necesitas para sumergirte en temas como la concurrencia con bastante rapidez. Tiene más aplicabilidad porque también puede orientar los conceptos de OO y web. También es bastante popular y obtendría que las compañías paguen por los libros de sus empleados, lo que siempre es bueno para las ventas ("Be a Kick Ass C # Programmer" va mucho más lejos 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 Esquema (bueno, no del todo, pero casi) y le brinda cierta capacidad para sumergirse en temas de POO, así como para engancharse en el .NET Framework para elementos de UI si desea darle un toque especial. Pero, en este momento, es oscuro.
No puedo hablar con Ruby, así que personalmente, mordería la bala e iría con C #.
Creo que usted debería tener bastante experiencia en el idioma 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 gran lenguaje para implementar cualquier concepto. Otras opciones pueden ser Erlang, Haskell, Ruby o Python, tal vez incluso algún dialecto ML. Estoy predispuesto en contra de la familia C (incluyendo C # y Java), parecen estar pegados a un nivel inferior de pensamiento sobre los conceptos.
Esa es una buena idea Creo que Scheme es una buena opción, ya que permite poner en práctica (en forma de bibliotecas) diferentes abstracciones con un mínimo indispensable. También es fácil traducir del esquema a un sistema de verificación como PVS ( http://pvs.csl.sri.com/ )
aclamaciones
Hay bastantes universidades que utilizan Perfect Developer para la enseñanza de métodos formales (exención de responsabilidad: estoy conectado con este producto). Está construido alrededor de un lenguaje para expresar especificaciones, refinamiento de datos y algoritmos. Cuenta con un probador de teoremas automático para verificación y un generador de código que puede producir C ++, C # y Java. El diseño de PD se inspiró en gran medida en "Una disciplina de programación", sin embargo, encontramos que la notación es poco práctica para los grandes sistemas, por lo que la notación se ha apartado algo de Dijktra.
Honestamente, no puedo recomendar a Ruby para esto. Cuando programo el día a día en mi mundo comercial, me gusta bastante, ciertamente mucho más que C o Java. Pero la semántica de la misma está tan mal definida que no confío en la mitad que en C, aunque puedo pasar varias horas discutiendo una declaración y consultando un libro blanco mucho más grueso que reemplazó a K&R. Termino bastante convencido de que si tengo un compilador conforme (sí, lo sé, soy un soñador, pero trabajo conmigo aquí) sé lo que está saliendo por el otro lado.
Ruby es maravilloso en muchos sentidos, pero en lo que se refiere a lo formal, los dos nunca se encontrarán.
Tendré a votar por Haskell, porque cada vez que me doy la vuelta me sorprende el sentido que tiene todo en esa definición de lenguaje. (Aunque hay que admitir 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 entiendo, también, lo dikjstra vs. lo funcional; volviendo y leyendo sus papeles está muy en un mundo imperativo; No estoy calificado para decir si realmente se fue por el camino equivocado. Tal vez solo estoy abrumado por lo buena que es su escritura, tanto como su pensamiento. Pero parecía complacerlo, ¿y qué hay de usar Algol 60 ?
Ignorando lo obvio, ¿cuáles son tus respuestas favorite language programming ?
Por un lado, está tratando de demostrar métodos a lo que se presume que son programadores intermedios. Si selecciona un solo idioma y lo bendice como el idioma de sus libros, posiblemente alejará a los lectores potenciales que no prefieren ese idioma por una razón u otra. Ya que está demostrando métodos, tiene el lujo de usar fragmentos de código en los idiomas que aparecen para ilustrar su punto de manera concisa. Por ejemplo, el único idioma disponible para demostrar RIIA es probablemente C ++, pero este mismo idioma es bastante malo para mostrar cómo realizar el análisis de origen. Scheme es ideal para el análisis de fuentes, pero no le brinda muchas opciones para explorar los beneficios (y las debilidades) de la tipificación fuerte. Usa muchos idiomas.
Por otro lado, ya que estás principalmente en los métodos de programación, no estoy totalmente seguro de que necesites un lenguaje real. Una notación bien definida es igual de buena y obliga a sus lectores a centrarse en el punto que está haciendo en lugar de los detalles superficiales de un idioma u otro.