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

Charlie,

Ich habe Dijkstras Meisterwerk immer mit einem Modell der Programmierung in Verbindung gebracht, bei dem Schleifen und Arrays im Mittelpunkt stehen. Wenn Sie sich eng an Dijkstra halten (z. B. bei der Berechnung der schwächsten Vorbedingungen), werden Sie feststellen, dass funktionale Sprachen nicht gut geeignet sind. Von den populären Sprachen, die eine gute Unterstützung für imperative Programmierung mit Schleifen und Arrays bieten, bringt Python vielleicht am wenigsten zusätzlichen Ballast mit sich.

Das soll nicht heißen, dass funktionale Sprachen für formale Methoden ungeeignet sind - sie sind sehr gut geeignet -, aber der Stil ist ganz anders als bei Dijkstra. Die bevorzugten Methoden legen den Schwerpunkt auf kalkulatorische Beweise; siehe Richard Birds Aufsatz über die Lösung von Sudoku (der es in sich hat) oder das Lehrbuch von Richard Bird und Phil Wadler.

Bei der Gleichzeitigkeit hängt es stark davon ab, an welches Modell der Gleichzeitigkeit (und welche formalen Methoden) Sie glauben. John Reppys Concurrent ML ist ein schönes Message-Passing-Modell. Erlang hat auch ein schönes, sauberes, restriktives Modell. Andererseits ist die Programmierung mit Sperren und kritischen Abschnitten so schwierig, dass formale Methoden in dieser Situation vielleicht mehr Nutzen bringen.

Zwei weitere Bemerkungen am Rande, die für Ihre Hintergrundrecherche von Interesse sein könnten:

• Der einzige Programmierer, den ich je getroffen habe, der Dijkstras Methoden in der Praxis auf reale Systeme angewandt hat, war Greg Nelson, der mit Modula-3 arbeitete. (Greg und Mark Manasse schrieben zusammen das Trestle-Fenstersystem.) Modula-3 war eine sehr schöne Sprache, die Digital durch Nachlässigkeit und Inkompetenz sterben ließ. Greg hatte ein schönes TOPLAS-Papier über eine Erweiterung von Dijkstras Kalkül.

• Die Modellierungssprache von Gerard Holzmann SPIN basiert direkt auf Dijkstras Sprache der bewachten Befehle und unterstützt auch die Gleichzeitigkeit. Ihr Zweck ist die Modellprüfung, nicht die Programmierung, und es gibt ein paar Eigenheiten, aber es gibt eine starke Verbindung zu formalen Methoden, und es ist wirklich großartig, dass man seine Behauptungen mit dem Modell prüfen kann. Jeder, der sich für formale Methoden interessiert, sollte sich das Programm einmal ansehen.

(Edit: Hier ist ein Link zum Greg Nelson Papier, oder eines von ihnen. - CRM)

Answer 2

Das Offensichtliche ignorieren, was ist Ihr Favorit Programmierung Sprache Antworten, sehe ich zwei nützliche Antworten:

Einerseits versuchen Sie, Methoden für vermeintlich fortgeschrittene Programmierer zu demonstrieren. Wenn Sie sich für eine einzige Sprache entscheiden und diese als Ihre Buchsprache anpreisen, verprellen Sie möglicherweise potenzielle Leser, die diese Sprache aus dem einen oder anderen Grund nicht bevorzugen. Da Sie Methoden demonstrieren, können Sie sich den Luxus erlauben, Schnipsel in Sprachen zu verwenden, die Ihren Standpunkt prägnant illustrieren. Zum Beispiel ist die einzige Sprache, die für die Demonstration von RIIA zur Verfügung steht, wahrscheinlich C++, aber dieselbe Sprache ist ziemlich schlecht, um zu zeigen, wie man eine Quelltextanalyse durchführt. Scheme ist ideal für die Quelltextanalyse, bietet aber nicht sehr viele Möglichkeiten, die Vorteile (und Schwächen) der starken Typisierung zu erkunden. Verwenden Sie viele Sprachen.

Andererseits bin ich mir nicht ganz sicher, ob Sie überhaupt eine richtige Sprache brauchen, da Sie sich hauptsächlich mit Methoden der Programmierung beschäftigen. Eine gut definierte Notation ist genauso gut und zwingt Ihre Leser dazu, sich auf das Wesentliche zu konzentrieren und nicht auf die oberflächlichen Details der einen oder anderen Sprache.

Answer 3

Ich bin mit Lisp und Scheme aufgewachsen und liebe sie beide. Ich denke, es sind großartige Sprachen, um sie von Grund auf zu lernen. Aber ich bin mir nicht sicher, ob jemand, der schon etwas Programmiererfahrung hat, mit diesen Sprachen etwas anfangen kann. Sie werden nicht viele Treffer auf Amazon für Ihr Buch mit Scheme im Titel erhalten :)

C# ist eine sehr einfach zu erlernende Sprache und bietet alle Grundlagen, die man braucht, um sich schnell in Themen wie Gleichzeitigkeit einzuarbeiten. Es hat mehr Anwendbarkeit, weil Sie OO und Web-Konzepte als auch zielen können. Außerdem ist sie recht populär, und die Unternehmen bezahlen ihren Mitarbeitern die Bücher, was immer gut für den Umsatz ist ("Be a Kick Ass C# Programmer" kommt auf einem Spesenabrechnungsbogen viel weiter als "Concurrency in Modern Lisp").

F# ist eine interessante Sprache. Sie hat die funktionale Schönheit von Lisp oder Scheme (na ja, nicht ganz, aber fast) und bietet die Möglichkeit, in OOP-Themen einzutauchen und das .NET Framework für UI-Zwecke zu nutzen, wenn man die Dinge aufpeppen möchte. Aber im Moment ist es obskur.

Ich kann nicht sagen, Ruby, so persönlich, ich würde in den sauren Apfel beißen und gehen mit C #.

Answer 4

Ehrlich gesagt, kann ich Ruby dafür nicht empfehlen. Wenn ich in meiner kommerziellen Welt tagtäglich programmiere, mag ich Ruby sehr, sicherlich viel mehr als C oder Java. Aber die Semantik ist so undefiniert, dass ich ihr nicht halb so viel Vertrauen entgegenbringe wie C, wo ich zwar mehrere Stunden damit verbringe, über eine Anweisung zu streiten und das viel dickere weiße Buch zu Rate zu ziehen, das K&R ersetzt hat, aber am Ende bin ich ziemlich überzeugt, dass ich weiß, was auf der anderen Seite herauskommt, wenn ich einen konformen Compiler habe (ja, ich weiß, ich bin ein Träumer, aber seien Sie mir da mal glauben).

Ruby ist in vielerlei Hinsicht wundervoll, aber wenn es um formale Dinge geht, werden sich die beiden nie begegnen.

Ich selbst würde eher für Haskell stimmen, denn jedes Mal, wenn ich mich umdrehe, bin ich erstaunt, wie viel Sinn alles in dieser Sprachdefinition macht. (Obwohl ich nach nur einem Jahr oder so sicher bin, dass ich noch nicht einmal die Hälfte der Ecken von Haskell 98 erforscht habe).

Und ich verstehe auch die Sache mit Dikjstra vs. funktional; zurückgehen und Lesen seiner Papiere Ich bin nicht in der Lage zu sagen, ob er dort wirklich den falschen Weg eingeschlagen hat. Vielleicht bin ich auch einfach nur überwältigt von der Qualität seiner Texte und seiner Gedanken. Aber es schien ihm zu gefallen, also was ist mit der Verwendung von Algol 60 ?

Answer 5

Das ist eine gute Idee. Ich denke, dass Scheme eine gute Option ist, da es einem erlaubt, verschiedene Abstraktionen mit einem Minimum an Grundlagen in die Praxis umzusetzen (in Form von Bibliotheken). Es ist auch einfach, von Scheme zu einem Verifikationssystem wie PVS ( http://pvs.csl.sri.com/ )

Prost