Ensinar métodos de programação e formais

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

Pergunta

Aqui está uma espécie de pergunta estranha. Eu estou no processo de escrever um livro sobre aprender a programar usando métodos formais, e eu estou indo para destiná-las para as pessoas com alguma experiência em programação. A ideia é ensiná-los a ser programadores de alta qualidade.

A notação básica vai ser de Disciplina de Dijkstra de Programação , juntamente com alguns simultaneidade e de comunicação extensões.

Ao contrário EWD, quero que meus alunos, eventualmente, para escrever programas executáveis ??reais. Isso significa que, em algum ponto tradução de notação EWD para algum outro idioma. Quando eu comecei a fazer a programação formais Segmentei C, mas você acaba escrevendo um monte de encanamento, e existem todas as complexidades de tratar ponteiros etc. Ruby é um alvo óbvio possível, como é Scheme ou Lisp. Mas há também as várias linguagens de função; desde que eu estou especialmente interessado em simultaneidade, Erlang parece ser uma possibilidade.

Então, finalmente, aqui está a minha pergunta:? Que língua (s) que eu deveria ensinar meus leitores para direcionar seus programas formalmente desenvolvidos

Foi útil?

Solução

Charlie,

Eu sempre associada obra-prima de Dijkstra com um modelo de programação em que o centro do palco é ocupado por loops e arrays. Se você está furando perto de Dijkstra (por exemplo, computação mais fracas condições) Eu acho que você vai encontrar linguagens funcionais não são um grande ajuste. Das linguagens populares que oferecem um bom suporte para programação imperativa com loops e arrays, talvez Python carrega a bagagem menos adicional.

Isto não quer dizer que linguagens funcionais são inadequados para métodos formais --- eles estão muito bem adaptado --- mas o estilo é muito diferente de Dijkstra. Os métodos preferidos enfatizar provas calculacional; veja papel Richard Bird em resolver Sudoku (que vai pesados) ou o livro de Richard Bird and Phil Wadler.

Para a simultaneidade que depende muito de qual é o modelo de concorrência (e que formal de métodos) que acredita. De John Reppy Concurrent ML é um modelo de passagem de mensagens bonito. Erlang também tem um modelo restritivo limpa agradável. Por outro lado, a programação com fechaduras e seções críticas é tão difícil, pode haver mais benefícios aos métodos formais nessa situação.

Duas outras observações de passagem, que podem ser de interesse para o seu fundo de investigação:

  • O único programador que eu já conheci que aplicaram métodos de Dijkstra na prática a sistemas reais foi Greg Nelson, que estava trabalhando em Modula-3. (Greg e Mark Manasse escreveu o sistema de janelas de cavalete juntos.) Modula-3 era uma língua muito agradável que Digital permitido morrer através fecklessness e incompetência. Greg teve um papel TOPLAS agradável em uma extensão para o cálculo de Dijkstra.

  • linguagem de modelagem de Gerard Holzmann SPIN é baseado diretamente na linguagem de comandos guardados de Dijkstra, e também suporta concorrência. Sua finalidade é a verificação de modelo, não de programação, e há algumas idiossincrasias, mas há uma forte ligação com os métodos formais, e é realmente ótimo para ser capaz de modelar verificar suas afirmações. Quem estiver interessado em métodos formais vai querer dar uma olhada.

(Edit: Aqui está um link para o Greg Nelson papel , ou um deles -. CRM)

Outras dicas

Eu cresci em Lisp e Scheme e amá-los tanto. Eu acho que eles são grandes línguas para aprender a partir do zero diante. Mas, eu não tenho certeza que alguém com alguma experiência em programação levaria para esses idiomas. Você não está indo para obter um monte de hits na Amazon para o seu livro com o esquema no título. :)

C # é uma linguagem muito fácil de aprender e tem todos os elementos básicos que você precisa para mergulhar em temas como a simultaneidade muito rapidamente. Ele tem mais aplicabilidade porque você pode direcionar conceitos OO e web também. Ele também é bastante popular e você obteria empresas pagando por seus empregados livros que é sempre bom para vendas ( "Seja um burro do pontapé C # Programmer" vai muito mais longe em uma folha de reembolso de despesas de "Concorrência em Modern Lisp").

F # é uma linguagem interessante. Tem a beleza funcional de um Lisp ou Scheme (bem, não é bem assim, mas quase) e dá-lhe alguma capacidade de mergulhar em tópicos OOP, bem como gancho para o .NET Framework para o material UI se você quiser apimentar as coisas. Mas, agora, é obscuro.

Eu não posso falar com Ruby, então, pessoalmente, gostaria de morder a bala e ir com C #.

Essa é uma idéia agradável. Acho Esquema é uma boa opção, pois permite um para colocar em prática (na forma de bibliotecas) diferentes abstrações com um nu mínimos essenciais. Também é fácil de tradução do esquema para um sistema de verificação como PVS ( http: //pvs.csl.sri. com / )

aplausos

Eu acho que você mesmo deve ter algum experiência na linguagem que você usa para o seu livro, ou alguém proficiente para rever o seu código.

Pessoalmente, eu usaria Lisp comum, desde que eu estou familiarizado com isso, e é uma grande linguagem de implementar qualquer conceito. Outras opções podem ser Erlang, Haskell, Ruby ou Python, talvez até algum dialeto ML. Estou tendenciosa contra a família C (incluindo C # e Java), eles parecem presos a um nível mais baixo de pensamento sobre conceitos.

Existem algumas universidades que utilizam Perfeito desenvolvedor para o ensino de métodos formais (disclaimer: Eu estou relacionados com este produto). Ele é construído em torno de uma linguagem para expressar especificações, refinamento de dados e algoritmos. Ele tem um provador de teoremas automático para verificação, e um gerador de código que pode produzir C ++, C # e Java. O projeto do PD foi muito inspirado por "A disciplina de Programação", no entanto, achamos a notação em vez impraticável para grandes sistemas, de modo a notação divergiu um pouco do Dijktra do.

Licenciado em: CC-BY-SA com atribuição
Não afiliado a StackOverflow
scroll top