Unterricht in Programmierung und formalen Methoden

Question

Ich habe eine etwas merkwürdige Frage. Ich bin gerade dabei, ein Buch über das Erlernen des Programmierens mit formalen Methoden zu schreiben, und ich werde es auf Leute mit einiger Programmiererfahrung ausrichten. Die Idee ist, ihnen beizubringen, hochwertige Programmierer zu werden.

Die grundlegende Notation wird von Dijkstra's Disziplin der Programmierung zusammen mit einigen Erweiterungen für Gleichzeitigkeit und Kommunikation.

Anders als bei der EWD möchte ich, dass meine Schüler letztendlich tatsächlich ausführbare Programme schreiben. Das bedeutet, dass sie irgendwann von der EWD-Notation in eine andere Sprache übersetzen müssen. Als ich mit dem formalen Programmieren anfing, habe ich C ins Auge gefasst, aber das bedeutet, dass man viel Klempnerarbeit leisten muss, und außerdem gibt es all die Komplexität bei der Behandlung von Zeigern usw. Ruby ist ein offensichtliches mögliches Ziel, ebenso wie Scheme oder Lisp. Aber es gibt auch die verschiedenen Funktionssprachen; da ich mich besonders für Gleichzeitigkeit interessiere, scheint Erlang eine Möglichkeit zu sein.

Nun zu meiner Frage: Welche Sprache(n) sollte(n) ich meinen Lesern beibringen, damit sie ihre formell entwickelten Programme gezielt einsetzen können?

Answer 1

Ich denke, dass Sie selbst einige Erfahrung in der Sprache haben sollten, die Sie für Ihr Buch verwenden, oder jemanden, der Ihren Code überprüfen kann.

Ich persönlich würde Common Lisp verwenden, da ich damit vertraut bin und es eine großartige Sprache ist, um jedes Konzept zu implementieren. Andere Optionen wären Erlang, Haskell, Ruby oder Python, vielleicht sogar ein ML-Dialekt. Ich bin voreingenommen gegenüber der C-Familie (einschließlich C# und Java), sie scheinen auf einer niedrigeren Ebene des Denkens über Konzepte festzustecken.

Answer 2

Es gibt eine ganze Reihe von Universitäten, die Perfect Developer für die Lehre formaler Methoden einsetzen (Haftungsausschluss: Ich bin mit diesem Produkt verbunden). Es basiert auf einer Sprache zur Formulierung von Spezifikationen, Datenverfeinerung und Algorithmen. Es verfügt über einen automatischen Theorembeweiser zur Überprüfung und einen Codegenerator, der C++, C# und Java erzeugen kann. Das Design von PD wurde stark von "A Discipline of Programming" inspiriert, allerdings fanden wir die Notation für große Systeme eher unpraktisch, so dass die Notation etwas von der von Dijktra abweicht.