Programmation pédagogique et 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 vers des 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 va être de Discipline of Programming de Dijkstra, avec quelques extensions de concurrence et de communications. Contrairement à EWD, je souhaite que mes élèves finissent par écrire des programmes exécutables réels. Cela signifie qu'à un certain moment, la traduction de la notation EWD vers une autre langue. Quand j'ai commencé à faire de la programmation formelle, j'ai ciblé C, mais vous avez fini par écrire beaucoup de plomberie, plus il y a toute la complexité du traitement des pointeurs, etc. Ruby est une cible possible, comme Scheme ou Lisp. Mais il y a aussi les différentes langues de fonction; puisque je suis particulièrement intéressé par la concurrence, Erlang semble être une possibilité. Donc, enfin, voici ma question: Quelle (s) langue (s) devrais-je enseigner à mes lecteurs pour cibler leurs programmes formellement développés?

Answer 1

Charlie,

J'ai toujours associé le chef-d'œuvre de Dijkstra avec un modèle de programmation dans lequel scène est occupée par des boucles et des tableaux. Si vous vous rapprochez de Dijkstra (par exemple, en calculant les conditions préalables les plus faibles), je pense que vous trouverez 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 sont inadapté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 du Sudoku (qui est lourd) ou le manuel de Richard Bird et Phil Wadler. Pour la simultanéité, cela dépend beaucoup du modèle de concurrence (et des méthodes formelles) auquel vous croyez. Le ML Concurrent de John Reppy est un beau modèle de passage de message. Erlang a aussi un beau modèle restrictif propre. D'autre part, la programmation avec des verrous et des sections critiques est si difficile, il peut y avoir plus d'avantages pour les méthodes formelles dans cette situation.

Deux autres remarques incidentes qui peuvent être d'intérêt pour votre recherche de fond:

• Le seul programmeur que j'ai jamais rencontré qui a appliqué les méthodes de Dijkstra dans la pratique des systèmes réels était Greg Nelson, qui travaillait à modulations 3. (Greg et Mark Manasse ont écrit le système de fenêtres Trestle ensemble.) Modula-3 était une très belle langue que Digital a permis de mourir à cause de l'imprudence et de l'incompétence. Greg avait un joli papier TOPLAS sur une extension du calcul de Dijkstra.

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

(Edit:. Voici un lien vers le papier Greg Nelson, ou l'un d'entre eux - CRM)

Answer 2

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

acclamations

Answer 3

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

C# est un langage très facile à apprendre et il a toutes les bases dont vous auriez besoin pour plonger assez rapidement dans des sujets tels que la concurrence. Il a plus d'applicabilité, car vous pouvez également cibler les concepts OO et Web. C'est aussi assez populaire et les entreprises paieraient pour leurs livres d'employés, ce qui est toujours bon pour les ventes («Be a Kick Ass C# Programmer» va beaucoup plus loin sur une feuille de remboursement de dépenses que «Concurrency in Lisp moderne»).

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 il vous donne la possibilité de plonger dans les sujets POO et de vous connecter au .NET Framework pour les choses si vous voulez pimenter les choses. Mais, en ce moment, c'est obscur.

Je ne peux pas parler à Ruby, donc personnellement, je mordre la balle et aller avec C#.

Answer 4

Je pense que vous devriez vous-même avoir une certaine expérience dans la langue que vous utilisez pour votre livre, ou quelqu'un de compétent pour examiner votre code.

Personnellement, j'utiliserais Common Lisp, puisque je suis familier avec cela, et c'est un excellent langage pour implémenter n'importe quel concept. D'autres options pourraient être Erlang, Haskell, Ruby, ou Python, peut-être même un peu de 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 5

Ignorant l'évidence ce qui est votre favoriteprogramminglanguage réponses, je vois deux réponses utiles:

D'une part, vous essayez de démontrer les méthodes à ce que sont présumés être les programmeurs intermédiaires.Si vous choisissez une seule langue et que vous la bénissez en tant que 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. Puisque vous démontrez des méthodes, vous avez le luxe d'utiliser des extraits dans des langues qui illustrent votre point de manière concise. Par exemple, le seul langage disponible pour démontrer RIIA est probablement C++, mais ce même langage est assez pauvre pour montrer comment effectuer une analyse de source. Le schéma est idéal pour l'analyse des sources, mais ne vous donne pas beaucoup d'options pour explorer les avantages (et les faiblesses) d'un typage fort. Utilisez plusieurs langues. D'autre part, puisque vous êtes principalement à la recherche de méthodes de programmation, je ne suis pas totalement 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 le point que vous faites plutôt que sur les détails superficiels d'une langue ou d'une autre.

Answer 6

Honnêtement, je ne peux pas recommander Ruby pour cela. Quand je programme au jour le jour dans mon monde commercial, j'aime beaucoup, certainement beaucoup plus que C ou Java.Mais la sémantique est si mal définie que je ne la crois pas autant que C où, bien que je puisse passer plusieurs heures à discuter d'une déclaration et consulter ce livre blanc beaucoup plus épais qui a remplacé K, je sors à la fin 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 sort de l'autre côté. Ruby est merveilleux à bien des égards, mais en ce qui concerne tout ce qui est formel, le twain ne se rencontrera jamais. J'aurais tendance à voter pour Haskell moi-même, parce que chaque fois que je me retourne, je suis étonné de voir à quel point tout ce qui fait sens dans cette définition de la langue. (Bien que je l'admet après seulement un an ou deux, je suis sûr que je n'ai pas exploré la moitié des coins de Haskell 98.)

Et je comprends aussi la chose fonctionnelle Dikjstra vs. revenir et reading his papers il est très dans un monde impératif; Je ne suis pas qualifié pour dire s'il a vraiment fait fausse route. Peut-être que je suis juste submergé par la qualité de son écriture, autant que sa pensée. Mais il a semblé lui plaire, alors qu'en est-il d'utiliser Algol 60?

Answer 7

Il existe plusieurs universités qui utilisent Perfect Developer pour enseigner des méthodes formelles (avertissement: je suis connecté avec ce produit). Il est construit autour d'un langage d'expression des spécifications, d'affinement des données et d'algorithmes. Il a un prouveur de théorème automatique pour la vérification, et un générateur de code qui peut produire C++, C# et Java. La conception de PD a été très inspirée par "A Discipline of Programming", mais nous avons trouvé la notation plutôt peu pratique pour les grands systèmes, donc la notation a quelque peu divergé de celle de Dijktra.