Enseignement de la programmation et des méthodes formelles

Question

Voici une sorte de question étrange. Je suis en train d'écrire un livre sur l'apprentissage de la programmation en utilisant des méthodes formelles, et je vais le cibler sur les personnes ayant une certaine expérience en programmation. L'idée est de leur apprendre à être des programmeurs de haute qualité.

La notation de base sera extraite de la discipline de la programmation de Dijkstra. avec quelques extensions de simultanéité et de communication.

Contrairement à EWD, je souhaite que mes étudiants écrivent éventuellement des programmes exécutables réels. Cela signifie qu’à un moment donné, la notation EWD est traduite dans une autre langue. Quand j'ai commencé à faire de la programmation formelle, je ciblais C, mais vous finissez par écrire beaucoup de plomberie, plus il y a toute la complexité de traiter les pointeurs, etc. Ruby est une cible possible évidente, tout comme Scheme ou Lisp. Mais il y a aussi les différents langages de fonctions; comme je suis particulièrement intéressé par la concurrence, Erlang semble être une possibilité.

Alors, enfin, voici ma question: Quelle (s) langue (s) dois-je apprendre à mes lecteurs pour cibler leurs programmes développés de manière formelle?

Answer 1

Charlie,

J'ai toujours associé le chef-d'œuvre de Dijkstra à un modèle de programmation dans lequel la scène centrale est occupée par des boucles et des tableaux. Si vous vous en tenez à Dijkstra (par exemple, en calculant les conditions préalables les plus faibles), vous constaterez que les langages fonctionnels ne conviennent pas. Parmi les langages populaires qui fournissent un bon support pour la programmation impérative avec des boucles et des tableaux, peut-être que Python porte le moins de bagage supplémentaire.

Cela ne veut pas dire que les langages fonctionnels ne sont pas adaptés aux méthodes formelles - ils sont très bien adaptés - mais le style est assez différent de Dijkstra. Les méthodes préférées mettent l’accent sur les preuves de calcul; voir l'article de Richard Bird sur la résolution de Sudoku (qui est lourd) ou le manuel de Richard Bird et Phil Wadler.

Pour la concurrence, cela dépend beaucoup du modèle de concurrence (et des méthodes formelles) auquel vous croyez. Concurrent ML de John Reppy est un beau modèle de transmission de messages. Erlang a également un modèle propre et restrictif. Par ailleurs, la programmation avec des verrous et des sections critiques est si difficile que les méthodes formelles pourraient présenter davantage d’avantages dans cette situation.

Deux autres remarques qui pourraient intéresser votre recherche de base:

• Le seul programmeur que j'ai jamais rencontré et qui appliquait les méthodes de Dijkstra en pratique à des systèmes réels était Greg Nelson, qui travaillait dans Modula-3. (Greg et Mark Manasse ont écrit ensemble le système de fenêtres à chevalets.) Modula-3 était un très beau langage que Digital a laissé mourir de chasteté et d'incompétence. Greg avait un bon papier TOPLAS sur une extension du calcul de Dijkstra.

• Le langage de modélisation de Gerard Holzmann, SPIN , est directement basé sur le langage de commandes protégées de Dijkstra, et il prend également en charge la concurrence. Son but est de vérifier les modèles, pas de programmer, et il y a quelques particularités, mais il existe un lien étroit avec les méthodes formelles, et c'est vraiment bien de pouvoir modéliser vos assertions. Toute personne intéressée par les méthodes formelles voudra le vérifier.

(Edit: voici un lien vers le Greg Nelson papier ou l’un d’eux. & # 8212; CRM)

Answer 2

Ignorer l'évident qu'est votre favori < a href = "https://stackoverflow.com/questions/273108/which-programming-languages-have-helped-you-to-understand-programming-better"> programmation language , je peux voir deux réponses utiles:

D'une part, vous essayez de montrer des méthodes à ce que l'on suppose être un programmeur intermédiaire. Si vous sélectionnez une seule langue et que vous la bénissez comme langue de vos livres, vous risquez d'aliéner les lecteurs potentiels qui ne préfèrent pas cette langue pour une raison ou une autre. Depuis que vous présentez des méthodes, vous avez le luxe d'utiliser des extraits dans des langues qui illustrent votre propos de manière concise. Par exemple, le seul langage disponible pour démontrer RIIA est probablement le C ++, mais ce même langage est assez médiocre pour montrer comment effectuer une analyse de source. Scheme est idéal pour l'analyse de la source, mais ne vous donne pas beaucoup d'options pour explorer les avantages (et les faiblesses) d'un typage puissant. Utilisez plusieurs langues.

D'un autre côté, comme vous maîtrisez principalement les méthodes de programmation, je ne suis pas tout à fait sûr que vous ayez besoin d'un vrai langage. Une notation bien définie est tout aussi bonne et oblige vos lecteurs à se concentrer sur ce que vous dites, plutôt que sur les détails superficiels d’une langue ou d’une autre.

Answer 3

J'ai grandi avec Lisp et Scheme et les aime tous les deux. Je pense que ce sont d'excellentes langues pour apprendre à partir de rien. Mais, je ne suis pas sûr que quelqu'un avec une certaine expérience en programmation utiliserait ces langues. Vous n'allez pas obtenir beaucoup de hits sur Amazon pour votre livre avec Scheme dans le titre. :)

C # est un langage très facile à apprendre. Il contient toutes les bases nécessaires pour se plonger assez rapidement dans des sujets tels que la concurrence. Il est plus applicable, car vous pouvez également cibler les concepts OO et Web. Il est également assez populaire et vous demanderiez aux entreprises de payer pour les livres de leurs employés, ce qui est toujours bon pour les ventes ("Soyez un programmeur Kick Ass C #" va beaucoup plus loin sur une feuille de remboursement des dépenses que "Accès simultané à Modern Lisp").

F # est une langue intéressante. Il a la beauté fonctionnelle d'un Lisp ou d'un Scheme (enfin, pas tout à fait, mais presque) et vous donne la possibilité de plonger dans des sujets de POO ainsi que de vous connecter au .NET Framework for UI si vous voulez pimenter les choses. Mais pour le moment, c'est obscur.

Je ne peux pas parler à Ruby, alors personnellement, je mordrais la balle et partirais avec C #.

Answer 4

Honnêtement, je ne peux pas recommander Ruby pour cela. Quand je programme au jour le jour dans mon monde commercial, je l’aime beaucoup, certainement beaucoup plus que C ou Java. Mais sa sémantique est si mal définie que je ne lui fais pas autant confiance que C où, bien que je puisse passer plusieurs heures à débattre au sujet d’une déclaration et à consulter un livre blanc beaucoup plus épais qui remplaçait K & R, je sors En fin de compte, je suis assez convaincu que si j’ai un compilateur conforme (oui, je sais, je suis un rêveur, mais travaille avec moi ici), je sais ce qui va sortir de l’autre côté.

Ruby est merveilleux à bien des égards, mais pour ce qui est formel, le twain ne se rencontrera jamais.

J'aurais tendance à voter pour Haskell moi-même, car chaque fois que je me retourne, je suis émerveillé par le sens que tout a de sens dans cette définition de langage. (Bien que, certes, après seulement un an ou plus, je suis sûr que je n’ai pas exploré la moitié des coins de même Haskell 98.)

Et je comprends aussi Dikjstra vs fonctionnel; en revenant sur sa lecture de ses papiers , il se trouvait vraiment dans un monde impératif; Je ne suis pas qualifié pour dire s'il s'est vraiment trompé. Peut-être suis-je juste dépassé par la qualité de ses écrits, autant que par ses pensées. Mais cela a semblé lui plaire, alors pourquoi ne pas utiliser Algol 60 ?

Answer 5

C'est une bonne idée. Je pense que Scheme est une bonne option car elle permet de mettre en pratique (sous forme de bibliothèques) différentes abstractions avec un minimum strict. Il est également facile de traduire un système en un système de vérification tel que PVS ( http: //pvs.csl.sri. com / )

acclamations

Answer 6

Je pense que vous devriez avoir vous-même une certaine expérience de la langue que vous utilisez pour votre livre ou une personne compétente pour réviser votre code.

Personnellement, j'utiliserais Common Lisp, car je le connais bien, et c’est un excellent langage pour mettre en œuvre n’importe quel concept. Les autres options peuvent être Erlang, Haskell, Ruby ou Python, voire un dialecte ML. Je suis partial contre la famille C (y compris C # et Java), ils semblent bloqués à un niveau inférieur de réflexion sur les concepts.

Answer 7

De nombreuses universités utilisent Perfect Developer pour enseigner des méthodes formelles (disclaimer: je suis connecté à ce produit). Il est construit autour d'un langage permettant d'exprimer les spécifications, le raffinement des données et des algorithmes. Il dispose d'un vérificateur automatique de théorèmes pour la vérification et d'un générateur de code capable de produire du C ++, du C # et du Java. La conception de la PD a été très inspirée par "Une discipline de programmation", mais nous avons trouvé que la notation était plutôt peu pratique pour les grands systèmes, elle a donc quelque peu divergé de celle de Dijktra.