プログラミングと形式的手法を教える

Question

ここで一種の奇妙な質問があります。私は現在、正式な手法を使ったプログラミング学習に関する本を執筆中ですが、ある程度のプログラミング経験のある人を対象にする予定です。その目的は、彼らに質の高いプログラマーになれるよう教えることです。

基本的な表記はダイクストラの表記となります。 プログラミングの規律, 、いくつかの同時実行性と通信拡張機能を備えています。

EWD とは異なり、私は生徒たちに最終的には実際の実行可能プログラムを書いてもらいたいと考えています。それは、ある時点で EWD 表記から他の言語に翻訳することを意味します。私が最初に正式なプログラミングを始めたときは C をターゲットにしていましたが、最終的には多くの配管を記述することになり、さらにポインターの処理などの複雑さが伴います。Ruby は、Scheme や Lisp と同様に、明らかにターゲットとなる可能性があります。しかし、さまざまな関数言語もあります。私は同時実行性に特に興味があるので、Erlang が可能性のように思えます。

それで、最後に私の質問は次のとおりです。正式に開発されたプログラムを対象とするために、読者にどの言語を教えるべきですか?

Answer 1

チャーリー、

私は、ダイクストラの傑作を、中央ステージがループとアレイで占められているプログラミングのモデルに常に関連付けてきました。ダイクストラの近くに固執している場合（たとえば、最も弱い前提条件を計算する場合）、関数型言語はあまり適していないと思います。ループと配列を使用した命令型プログラミングの適切なサポートを提供する一般的な言語の中で、おそらくPythonは追加の手荷物を最小限に抑えています。

これは、関数型言語が形式的なメソッドに適していないということではありません---それらは非常に適しています---スタイルはダイクストラとはまったく異なります。好ましい方法は、計算上の証明を強調します。数独の解決に関するリチャードバードの論文（これは大変だ）またはリチャードバードとフィルワドラーの教科書を参照してください。

並行性については、並行性のモデル（および正式な方法）に大きく依存します。JohnReppyのConcurrent MLは美しいメッセージ受け渡しモデルです。 Erlangには、きれいで制限的なモデルもあります。一方、ロックとクリティカルセクションを使用したプログラミングは非常に困難であるため、そのような状況では正式なメソッドを使用する方がメリットがある場合があります。

あなたの背景研究に興味があるかもしれない他の2つの合格した発言：

• 実際にダイクストラの方法を実際のシステムに適用したのは、Modula-3で働いていたGreg Nelsonだけでした。 （グレッグとマークマナスは、トレスルウィンドウシステムを一緒に作成しました。） Modula-3は、Digitalが無秩序と無能によって死ぬことを許した非常に素晴らしい言語でした。グレッグはダイクストラの微積分の拡張に関する素晴らしいTOPLAS論文を持っていました。

• Gerard Holzmannのモデリング言語 SPIN は、Dijkstraの保護されたコマンドの言語に直接基づいています。また、並行性もサポートします。その目的はプログラミングではなくモデルチェックであり、いくつかの特異性がありますが、形式的なメソッドとの強いつながりがあり、アサーションをモデルチェックできることは本当に素晴らしいことです。正式な方法に興味がある人は、ぜひチェックしてみてください。

（編集：グレッグネルソンへのリンクです。 紙、またはそれらの1つ＆＃8212; CRM）

Answer 2

あなたのお気に入り < a href = "https://stackoverflow.com/questions/273108/which-programming-languages-have-helped-you-to-understand-programming-better">プログラミング 言語の回答には、2つの有用な回答があります：

一方で、あなたは中間プログラマーであると推定されるものに対してメソッドを実証しようとしています。単一の言語を選択し、それを本の言語として祝福すると、何らかの理由でその言語を好まない可能性のある読者を疎外する可能性があります。メソッドをデモンストレーションしているため、言語でスニペットを使用して、ポイントを簡潔に示すことができます。たとえば、RIIAのデモンストレーションに使用できる言語はおそらくC ++だけですが、この同じ言語はソース分析の実行方法を示すにはかなり貧弱です。 Schemeはソース分析に理想的ですが、厳密な型指定の利点（および弱点）を調査するためのオプションはあまり多くありません。多くの言語を使用します。

一方、あなたは主にプログラミングの方法に依存しているため、実際の言語が必要かどうかはまったくわかりません。明確に定義された表記法も同様に優れており、読者はある言語または別の言語の表面的な詳細ではなく、あなたが作成しているポイントに集中するように強制します。

Answer 3

私はLispとSchemeで育ち、その両方が大好きです。ゼロから学ぶのに最適な言語だと思います。しかし、プログラミングの経験がある人がそれらの言語を使用するかどうかはわかりません。あなたは、タイトルにSchemeを含むあなたの本のAmazonで多くのヒットを得ることはないでしょう。 ：）

C＃は非常に習得しやすい言語であり、同時実行性などのトピックにすばやく飛び込むために必要なすべての基本を備えています。オブジェクト指向とWebの概念もターゲットにできるため、より多くの適用性があります。また、非常に人気があり、会社は従業員の本にお金を払ってもらえますが、これは常に販売に適しています（「Be a Kick Ass C＃Programmer」」は、「Concurrentency in Modern Lisp」よりもはるかに経費の払い戻しシートに記載されています）

F＃は興味深い言語です。 LispやSchemeの機能的な美しさを備えており（まったくそうではありませんが、ほとんど）、OOPトピックに飛び込むことができ、物事を盛り上げたい場合はUIの.NET Frameworkにフックすることができます。しかし、今のところ、あいまいです。

Rubyと話すことができないので、個人的には、弾丸を噛んでC＃を使います。

Answer 4

正直なところ、Ruby はこれにはお勧めできません。私は商業の世界で日々プログラミングするとき、C や Java よりもプログラミングがとても好きです。しかし、そのセマンティクスは非常に不明確なので、私は C の半分も信頼していません。C では、ステートメントについて議論したり、K&R に代わる分厚い白書を調べたりするのに数時間を費やすかもしれませんが、最後に、準拠したコンパイラを持っていれば (はい、わかっています。私は夢想家ですが、ここで協力してください)、反対側で何が起こるかがわかるとかなり確信しています。

ルビーは多くの点で素晴​​らしいですが、正式なことに関して言えば、二人が出会うことは決してありません。

私自身、Haskell に投票する傾向があります。なぜなら、振り向くたびに、その言語定義ですべてがどれほど理にかなっているかに驚かれるからです。(とはいえ、実際に使い始めてからわずか 1 年ほどですが、Haskell 98 ですら隅の半分も探索していないはずです。)

そしてディクストラ対ディクストラのことも理解しています。機能的なもの。戻って、そして 彼の論文を読んでいる 彼は非常に命令的な世界にいます。彼がそこで本当に道を間違えたかどうかを言う資格は私にはありません。おそらく私は、彼の思想と同じくらい、彼の文章の素晴らしさに圧倒されているだけなのかもしれません。でも、彼は気に入ったようなので、どうしたらいいでしょうか？ アルゴル60?

Answer 5

それはいいアイデアです。 Schemeは、最低限の必要事項を備えたさまざまな抽象化を（ライブラリーの形で）実践できるため、良い選択肢だと思います。 スキームからPVS（ http：//pvs.csl.sriのような検証システムへの変換も簡単です。 com / ）

歓声

Answer 6

自分が本に使用する言語でかなりの経験を積んでいるか、コードをレビューするのに熟練した人である必要があると思います。

個人的には、Common Lispを使います。それは、私がそれをよく知っているからであり、どんな概念を実装するのにも素晴らしい言語です。他のオプションとしては、Erlang、Haskell、Ruby、またはPythonがあり、ML方言もあります。私はCファミリ（C＃とJavaを含む）に偏っており、コンセプトについてのより低いレベルの思考に固執しているようです。

Answer 7

正式な方法を教えるためにPerfect Developerを使用している大学はかなりあります（免責事項：私はこの製品に関連しています）。仕様、データの洗練、アルゴリズムを表現するための言語を中心に構築されています。検証用の自動定理証明器と、C ++、C＃、およびJavaを生成できるコードジェネレーターがあります。 PDの設計は「プログラミングの規律」に非常に触発されましたが、表記法は大規模なシステムでは実用的ではないことがわかったため、表記法はダイクトラのものとは多少異なります。