Programación docente y métodos formales.

Question

Aquí hay una especie de pregunta extraña. Estoy en el proceso de escribir un libro sobre aprender a programar usando métodos formales, y voy a apuntarlo a personas con algo de 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 concurrencias y extensiones de comunicaciones.

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

Entonces, finalmente, esta es mi pregunta: ¿Qué idioma (s) debo enseñar a mis lectores para que apunten a sus programas desarrollados formalmente?

Answer 1

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 matrices. Si te quedas cerca de Dijkstra (por ejemplo, calculando las precondiciones más débiles), creo que encontrarás que los lenguajes funcionales no encajan. De los lenguajes populares que brindan 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 no sean adecuados para los métodos formales --- son muy adecuados --- pero el estilo es bastante 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 pesado) o el libro de texto de Richard Bird y Phil Wadler.

Para la concurrencia, depende mucho de qué modelo de concurrencia (y qué métodos formales) creas. El Concurrent ML de John Reppy es un hermoso modelo para pasar mensajes. Erlang también tiene un bonito modelo limpio y restrictivo. Por otro lado, programar 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 aprobados 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 estaba trabajando 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 impotencia y la incompetencia. Greg tenía un bonito 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 es compatible con la concurrencia. Su propósito es la verificación del modelo, no la programación, y hay algunas idiosincrasias, pero hay una fuerte conexión con los métodos formales, y es realmente genial poder verificar las afirmaciones del modelo. Cualquier persona interesada en métodos formales querrá echarle un vistazo.

(Editar: aquí hay un enlace a Greg Nelson papel, o uno de ellos. - CRM)

Answer 2

Ignorando lo obvio, ¿cuál es tu favorito < a href = "https://stackoverflow.com/questions/273108/which-programming-languages-have-helped-you-to-understand-programming-better"> programación language respuestas, puedo ver dos respuestas útiles:

Por un lado, está intentando demostrar métodos a lo que se supone que son programadores intermedios. Si selecciona un solo idioma y lo bendice como el idioma de sus libros, posiblemente alienará a los lectores potenciales que no prefieren ese idioma por una razón u otra. Como está demostrando métodos, tiene el lujo de usar fragmentos en idiomas que ilustran su punto de manera 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 el análisis de origen. Scheme es ideal para el análisis de origen, pero no le brinda muchas opciones para explorar los beneficios (y las debilidades) de la escritura fuerte. Usa muchos idiomas.

Por otro lado, dado que usted es principalmente experto en métodos de programación, no estoy totalmente seguro de que necesite ningún 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.

Answer 3

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 algo de experiencia en programación tome esos lenguajes. No obtendrá muchos éxitos en Amazon para su 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 de OO y web. También es bastante popular y las compañías pagarían 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 `` Concurrencia en Modern Lisp '').

F # es un lenguaje interesante. Tiene la belleza funcional de un Lisp o Scheme (bueno, no del todo, pero casi) y le brinda cierta capacidad para sumergirse en temas de OOP, así como conectarse al .NET Framework para cosas de UI si desea condimentar las cosas. Pero, en este momento, es oscuro.

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

Answer 4

Honestamente, no puedo recomendar a Ruby para esto. Cuando programo día a día en mi mundo comercial, me gusta bastante, ciertamente mucho más que C o Java. Pero la semántica está tan mal definida que no confío en la mitad de lo que C, aunque puedo pasar varias horas discutiendo sobre una declaración y consultando ese libro blanco mucho más grueso que reemplazó a K & amp; R, salgo al final estoy bastante convencido de que si tengo un compilador conforme (sí, lo sé, soy un soñador, pero trabaja conmigo aquí) sé lo que está saliendo del otro lado.

Ruby es maravilloso en muchos sentidos, pero en lo que respecta a todo lo formal, los dos nunca se encontrarán.

Tiendo a votar por Haskell yo mismo, porque cada vez que me doy la vuelta me sorprende lo mucho que tiene sentido todo en esa definición de 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 incluso Haskell 98.)

Y también entiendo lo de Dikjstra vs. lo funcional; volviendo atrás y leyendo sus documentos está muy en un mundo imperativo; No estoy calificado para decir si realmente fue por el camino equivocado. Quizás estoy abrumado por lo bueno que es su escritura, tanto como su pensamiento. Pero parecía complacerlo, entonces, ¿qué pasa con el uso de Algol 60 ?

Answer 5

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 esencial. También es fácil traducir del esquema a un sistema de verificación como PVS ( http: //pvs.csl.sri. com / )

aplausos

Answer 6

Creo que usted mismo debería tener bastante experiencia en el idioma que utiliza 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 de ML. Estoy predispuesto en contra de la familia C (incluyendo C # y Java), parecen atascados en un nivel inferior de pensamiento sobre conceptos.

Answer 7

Hay bastantes universidades que usan Perfect Developer para enseñar métodos formales (descargo de responsabilidad: estoy conectado con este producto). Está construido alrededor de un lenguaje para expresar especificaciones, refinamiento de datos y algoritmos. Tiene un comprobador 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ó mucho en "Una 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 desviado un poco de la de Dijktra.