プログラミングは単なるコーディングではありません

この記事は翻訳です スタンフォードセミナー。 しかし、彼女の前に少し自己紹介があります。 ゾンビはどのように形成されるのでしょうか？ 誰もが、友人や同僚を自分のレベルまで引き上げたいと思うかもしれませんが、それはうまくいきません。 そして、「うまくいかない」のは、あなたの場合よりも彼の場合です。一方には通常の給与、仕事などがあり、もう一方には考える必要があります。 考えることは不快で苦痛です。 彼はすぐに諦めて、まったく頭を働かせずにコードを書き続けます。 学習性無力感の壁を乗り越えるのにどれだけの努力が必要かを想像しているのに、それを実行しないだけです。 このようにしてゾンビが形成され、それを治すことができるようですが、誰もそれをやらないようです。

それを見たとき レスリー・ランポート （そう、教科書に登場する同志です） ロシアに来る と報告ではなく質疑応答をするのですが、少し警戒しました。 念のため言っておきますが、レスリーは世界的に有名な科学者であり、分散コンピューティングの基礎的な著作の著者であり、LaTeX の「Lamport TeX」という単語の La という文字でも彼を知ることができます。 XNUMX 番目の憂慮すべき要因は、彼の要求です。来る人は全員 (完全に無料で) 事前に彼の報告をいくつか聞き、それについて少なくとも XNUMX つの質問を考えてから来る必要があります。 そこでランポートが何を放送しているのか見てみることにしました - そしてそれは素晴らしいものでした! まさにそれ、ゾンビを治す魔法のリンクピルです。 警告しますが、本文からわかるように、非常に柔軟な方法論を愛する人や、書かれていることをテストするのが好きではない人は、著しく燃え尽きてしまう可能性があります。

実際、ハブロカットの後、セミナーの翻訳が始まります。 読書を楽しむ！

どのようなタスクに取り組む場合でも、常に次の XNUMX つのステップを実行する必要があります。

• 達成したい目標を決めます。
• 目標を達成する方法を決定します。
• あなたの目標に来てください。

これはプログラミングにも当てはまります。 コードを記述するときは、次のことを行う必要があります。

• プログラムが何をすべきかを決定します。
• そのタスクをどのように実行するかを決定します。
• 対応するコードを書きます。

もちろん最後のステップは非常に重要ですが、今日はそれについては話しません。 代わりに、最初の XNUMX つについて説明します。 すべてのプログラマーは作業を開始する前にこれらを実行します。 ブラウザを書くのかデータベースを書くのかを決めなければ、座って書くことはできません。 目標についての特定のアイデアが存在する必要があります。 そして、プログラムが具体的に何をするのかをよく考えて、コードが何らかの形でブラウザに変わることを期待してコードを作成しないでください。

このコードの事前検討は具体的にどのように行われるのでしょうか? これにどれだけの努力をすべきでしょうか？ それはすべて、解決しようとしている問題がどれだけ複雑かによって決まります。 フォールトトレラントな分散システムを作成したいとします。 この場合、コードを作成する前に、慎重に検討する必要があります。 整数変数を 1 だけインクリメントする必要がある場合はどうなるでしょうか? 一見すると、ここではすべてが些細なことなので考える必要はありませんが、オーバーフローが発生する可能性があることを思い出します。 したがって、問題が単純なのか複雑なのかを理解するためにも、まず考える必要があります。

問題に対する考えられる解決策を事前に考えておけば、間違いを避けることができます。 ただし、これには思考が明確であることが必要です。 これを達成するには、自分の考えを書き留める必要があります。 私はディック・ギンドンの次の言葉がとても好きです。「あなたが文章を書くと、自然はあなたの思考がどれほどずさんであるかを教えてくれます。」 書かないと考えているとしか思えない。 そして、自分の考えを仕様書の形で書き留める必要があります。

仕様は、特に大規模なプロジェクトで多くの機能を実行します。 しかし、私はそれらのうちの XNUMX つについてのみ話します。それらは私たちが明確に考えるのに役立ちます。 明確に考えることは非常に重要ですが、非常に難しいため、ここでは助けが必要です。 仕様は何語で書くべきですか? 一般に、プログラマーにとって常に最初の質問は、「どの言語で書くか」です。 これに対する唯一の正解はありません。私たちが解決している問題はあまりにも多様です。 一部の人にとって、TLA+ は私が開発した仕様言語です。 その他の場合は、中国語を使用する方が便利です。 すべては状況次第です。

さらに重要なのは、より明晰な思考を達成するにはどうすればよいかという別の質問です。 回答: 私たちは科学者のように考えなければなりません。 これは過去 500 年にわたって実証されてきた考え方です。 科学では、現実の数学的モデルを構築します。 天文学はおそらく、厳密な意味での最初の科学でした。 天文学で使用される数学モデルでは、天体は質量、位置、運動量を持った点として見えますが、実際には山や海、潮汐などを含む非常に複雑な天体です。 このモデルは、他のモデルと同様、特定の問題を解決するために作成されました。 惑星を見つける必要がある場合に、望遠鏡をどこに向けるかを決定するのに最適です。 しかし、地球上の天気を予測したい場合、このモデルは機能しません。

数学を使用すると、モデルのプロパティを決定できます。 そして科学は、これらの特性が現実とどのように関係しているかを示しています。 私たちの科学、コンピューターサイエンスについて話しましょう。 私たちが実際に使用しているのは、プロセッサー、ゲーム機、コンピューター、プログラムの実行など、さまざまな種類のコンピューティング システムです。 コンピューター上でのプログラムの実行について説明しますが、概して、これらの結論はすべて、どのコンピューター システムにも当てはまります。 私たちの科学では、チューリング マシン、部分的に順序付けられた一連のイベントなど、さまざまなモデルが使用されています。

プログラムとは何ですか? これは、独立して考慮できる任意のコードです。 ブラウザを作成する必要があるとします。 私たちは XNUMX つのタスクを実行します。ユーザーから見たプログラムの見方を設計し、次にプログラムの概要図を作成し、最後にコードを作成します。 コードを書いていくと、テキスト フォーマッタを作成する必要があることがわかります。 ここでも XNUMX つの問題を解決する必要があります。このツールがどのようなテキストを返すかを決定します。 フォーマットのアルゴリズムを選択します。 コードを書きます。 このタスクには、単語にハイフンを正しく挿入するという独自のサブタスクがあります。 このサブタスクも XNUMX つのステップで解決します。ご覧のとおり、これらのステップは多くのレベルで繰り返されます。

最初のステップ、つまりプログラムがどのような問題を解決するのかをさらに詳しく考えてみましょう。 ここでは、ほとんどの場合、何らかの入力を受け取り、何らかの出力を生成する関数としてプログラムをモデル化します。 数学では、関数は通常、順序付けられたペアのセットとして記述されます。 たとえば、自然数の二乗関数は集合 {<0,0>, <1,1>, <2,4>, <3,9>, …} として記述されます。 このような関数の定義域は、各ペアの最初の要素のセット、つまり自然数です。 関数を定義するには、そのスコープと式を指定する必要があります。

ただし、数学の関数はプログラミング言語の関数と同じではありません。 計算はずっと簡単です。 複雑な例について説明する時間がないので、単純な例を考えてみましょう。XNUMX つの整数の最大公約数を返す C の関数または Java の静的メソッドです。 このメソッドの仕様では、次のように書きます。 GCD(M,N) 引数用 M и Nどこ GCD(M,N) - ドメインが整数のペアのセットであり、戻り値が次の値で割り切れる最大の整数である関数。 M и N。 このモデルは現実とどのように関係するのでしょうか? モデルは整数で動作しますが、C または Java では 32 ビットの整数が使用されます。 int。 このモデルにより、アルゴリズムが正しいかどうかを判断できます GCD, ただし、オーバーフローエラーは防止できません。 これには、より複雑なモデルが必要になりますが、時間がありません。

モデルとしての関数の制限について話しましょう。 一部のプログラム (オペレーティング システムなど) は、特定の引数に対して特定の値を返すだけでなく、継続的に実行できます。 さらに、モデルとしての機能は、問題の解決方法を計画するという XNUMX 番目のステップにはあまり適していません。 クイック ソートとバブル ソートは同じ関数を計算しますが、それらはまったく異なるアルゴリズムです。 したがって、プログラムの目標がどのように達成されるかを説明するために、別のモデルを使用します。これを標準動作モデルと呼びます。 その中のプログラムは、許容されるすべての動作のセットとして表され、それぞれが一連の状態であり、その状態は変数への値の割り当てです。

Euclid アルゴリズムの XNUMX 番目のステップがどのようなものになるかを見てみましょう。 計算する必要があります GCD(M, N)。 初期化する M 方法 xと N 方法 y、次に、これらの変数の大きい方から小さい方を繰り返し、等しくなるまで減算します。 たとえば、次の場合 M = 12と N = 18、次の動作を説明できます。

[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]

そしてもし M = 0 и N = 0? ゼロはすべての数値で割り切れるため、この場合の最大約数はありません。 この状況では、最初のステップに戻って、正でない数値の GCD を計算する必要があるかどうかを尋ねる必要があります。 必要がない場合は仕様を変更するだけで済みます。

ここで、生産性について少し余談をしておきます。 多くの場合、XNUMX 日に書かれたコードの行数で測定されます。 ただし、一定数の行を削除すると、バグが入り込む余地が少なくなるため、作業がより有用になります。 コードを削除する最も簡単な方法は、最初のステップです。 実装しようとしている付加機能のすべてが必要ない可能性は十分にあります。 プログラムを簡素化し、時間を節約する最も簡単な方法は、実行すべきではないことを実行しないことです。 XNUMX 番目のステップは、XNUMX 番目に時間を節約できる可能性があります。 書かれた行数で生産性を測定する場合、タスクを達成する方法を考えることで、 生産性が低いなぜなら、同じ問題をより少ないコードで解決できるからです。 ここで正確な統計を示すことはできません。仕様書、つまり最初と XNUMX 番目のステップに時間を費やしたために書かなかった行数を数える方法がないからです。 また、実験では最初のステップを完了する権利がなく、タスクが事前に決められているため、ここでも実験をセットアップすることはできません。

非公式仕様では多くの問題が見落とされがちです。 関数の厳密な仕様を記述することは何も難しいことではありません。これについては説明しません。 代わりに、標準の動作に対する強力な仕様の作成について説明します。 あらゆる一連の動作はセキュリティ プロパティを使用して記述できるという定理があります。 （安全性） 生存性特性 (生き生き)。 セキュリティとは、何も悪いことが起こらず、プログラムが間違った答えを与えないことを意味します。 生存可能性とは、遅かれ早かれ何か良いことが起こること、つまりプログラムが遅かれ早かれ正しい答えを与えることを意味します。 原則として、セキュリティはより重要な指標であり、エラーが最も頻繁に発生するのはここです。 したがって、時間を節約するために、生存可能性については話しませんが、もちろんそれも重要です。

まず、可能な初期状態のセットを規定することでセキュリティを実現します。 そして XNUMX 番目に、各状態で考えられるすべての次の状態との関係です。 科学者のように行動して、状態を数学的に定義してみましょう。 初期状態のセットは、たとえば Euclid アルゴリズムの場合、次の式で記述されます。 (x = M) ∧ (y = N)。 特定の値については M и N 初期状態は XNUMX つだけです。 次の状態との関係は、次の状態の変数にはプライムを付けて記述し、現在の状態の変数にはプライムを付けずに記述する式で記述されます。 Euclid のアルゴリズムの場合、XNUMX つの式の論理和を扱います。そのうちの XNUMX つは x が最大値で、XNUMX 番目の値は - y:

最初のケースでは、y の新しい値は y の以前の値と等しく、大きい変数から小さい変数を減算することで x の新しい値が得られます。 XNUMX 番目のケースでは、その逆を行います。

Euclid のアルゴリズムに戻りましょう。 もう一度仮定してみましょう M = 12, N = 18。 これは単一の初期状態を定義します。 (x = 12) ∧ (y = 18)。 次に、これらの値を上記の式に代入すると、次の結果が得られます。

考えられる唯一の解決策は次のとおりです。 x' = 18 - 12 ∧ y' = 12すると次のような動作が得られます。 [x = 12, y = 18]。 同様に、行動におけるすべての状態を記述することができます。 [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].

最後の状態で [x = 6, y = 6] 式の両方の部分が false になるため、次の状態はありません。 これで、XNUMX 番目のステップの完全な仕様が完成しました。ご覧のとおり、これはエンジニアや科学者のようなごく普通の数学であり、コンピューター サイエンスのような奇妙ではありません。

これら XNUMX つの式は、時相論理の XNUMX つの式に組み合わせることができます。 彼女はエレガントで説明しやすいのですが、今は時間がありません。 時相ロジックは活気のプロパティにのみ必要であり、セキュリティには必要ありません。 私は時相論理そのものが好きではありません。それはまったく普通の数学ではありませんが、活気の場合には必要悪です。

Euclid のアルゴリズムでは、各値に対して x и y 独特の価値観を持っている x' и y'、次の状態との関係が true になります。 言い換えれば、Euclid のアルゴリズムは決定論的です。 非決定的アルゴリズムをモデル化するには、現在の状態に複数の可能な将来の状態があり、次の状態との関係が真となるように、各プライムされていない変数値が複数のプライムされた変数値を持っている必要があります。 これは簡単ですが、ここでは例を示しません。

実用的なツールを作成するには、正式な数学が必要です。 仕様を正式なものにするにはどうすればよいでしょうか? これを行うには、次のような形式言語が必要です。 TLA +。 Euclid アルゴリズムの仕様は、この言語では次のようになります。

三角形の付いた等号記号は、符号の左側の値が符号の右側の値と等しいように定義されていることを意味します。 本質的に、仕様は XNUMX つの定義であり、この場合は XNUMX つの定義です。 TLA+ の仕様には、上のスライドにあるように、宣言といくつかの構文を追加する必要があります。 ASCII では次のようになります。

ご覧のとおり、複雑なことは何もありません。 TLA+ の仕様はテストできます。つまり、小規模モデルで考えられるすべての動作をバイパスできます。 私たちの場合、このモデルは特定の値になります M и N。 これは、完全に自動化された非常に効率的で簡単な検証方法です。 正式な真実証明を書いて機械的にチェックすることも可能ですが、非常に時間がかかるため、これを行う人はほとんどいません。

TLA+ の主な欠点は、それが数学であり、プログラマーやコンピューター科学者が数学を恐れていることです。 一見すると冗談のように聞こえますが、残念ながらこれは本気で言っています。 私の同僚は、数人の開発者に TLA+ についてどのように説明しようとしたかを私に話してくれました。 数式が画面に表示されるとすぐに、彼らはすぐにガラスのような目になりました。 TLA+ が怖い場合は、以下を使用できます。 プラスカル、それは一種のおもちゃのプログラミング言語です。 PlusCal の式には、任意の TLA+ 式、つまり、概して任意の数学式を使用できます。 さらに、PlusCal には非決定的アルゴリズム用の構文があります。 PlusCal は任意の TLA+ 式を記述できるため、実際のプログラミング言語よりもはるかに表現力が豊かです。 次に、PlusCal は読みやすい TLA+ 仕様にコンパイルされます。 もちろん、これは複雑な PlusCal 仕様が TLA + 上で単純なものに変わるという意味ではありません。単にそれらの間の対応が明らかであり、追加の複雑さはありません。 最後に、この仕様は TLA+ ツールによって検証できます。 全体として、PlusCal は数学恐怖症の克服に役立ち、プログラマーやコンピューター科学者にとっても理解しやすいものです。 過去に、私はしばらくの間 (約 10 年)、それに関するアルゴリズムを公開しました。

おそらく誰かが、TLA + と PlusCal は数学であり、数学は発明された例でのみ機能する、と反論するでしょう。 実際には、型、プロシージャ、オブジェクトなどを備えた実際の言語が必要です。 これは間違っています。 Amazonで働いていたクリス・ニューカム氏はこう書いています。 「私たちは XNUMX 件の主要プロジェクトで TLA+ を使用しましたが、いずれの場合も、本番環境に入る前に危険なバグを発見でき、開発に必要な洞察と自信が得られたため、TLA+ を使用することで開発に大きな違いが生じました。プログラムの真実に影響を与えることなく、積極的なパフォーマンスの最適化を行います。」。 形式的なメソッドを使用すると非効率なコードが生成されるという話をよく聞きますが、実際にはすべてがまったく逆です。 また、プログラマーは形式的手法の有用性を確信していても、管理者は形式的手法の必要性を納得できないという意見もあります。 そしてニューカムはこう書いている。 「マネージャーは現在、TLA + の仕様の作成に熱心に取り組んでおり、特にこれに時間を割り当てています。」。 したがって、マネージャーは TLA+ が機能していることを確認すると、喜んでそれを受け入れます。 Chris Newcomb がこれを約 2014 か月前 (14 年 10 月) に書きましたが、現在、私の知る限り、TLA+ は 360 ではなく 360 のプロジェクトで使用されています。もう XNUMX つの例は、XBox XNUMX の設計に関連しています。Charles Thacker のところにインターンが来て、メモリシステムの仕様を書きました。 この仕様のおかげで、通常なら気づかれないバグが発見され、そのせいですべての XBox XNUMX が XNUMX 時間使用するとクラッシュしてしまいました。 IBM のエンジニアは、テストではこのバグが見つからなかったことを確認しました。

TLA + についてはインターネットで詳しく読むことができますが、ここでは非公式の仕様について説明しましょう。 最小公倍数などを計算するプログラムを作成する必要はほとんどありません。 私が TLA+ 用に書いたプリティ プリンタ ツールのようなプログラムを書くことのほうがずっと多いです。 最も単純な処理後の TLA + コードは次のようになります。

しかし、上記の例では、ユーザーはおそらく接続詞と等号を揃えたいと考えています。 したがって、正しい書式は次のようになります。

別の例を考えてみましょう：

ここでは逆に、ソース内の等号、加算、乗算の記号の配置がランダムであるため、最も単純な処理で十分です。 一般に、正しい書式設定の正確な数学的定義はありません。この場合の「正しい」とは「ユーザーが望むもの」を意味し、これを数学的に決定することはできないからです。

真実の定義がなければ、仕様は役に立たないように思えます。 しかし、そうではありません。 プログラムが何をするべきかわからないからといって、それがどのように機能するかを考える必要がないという意味ではありません。それどころか、プログラムにさらに努力する必要があります。 ここでは仕様が特に重要です。 構造化印刷に最適なプログラムを決定することは不可能ですが、構造化印刷をまったく取り入れてはいけないという意味ではなく、意識の流れとしてコードを書くことは良いことではありません。 最終的に、定義を含む XNUMX つのルールの仕様を作成しました。 コメントの形で Java ファイル内。 以下にルールの XNUMX つの例を示します。 a left-comment token is LeftComment aligned with its covering token。 このルールは、いわば数学英語で書かれています。 LeftComment aligned, left-comment и covering token - 定義付きの用語。 これが数学者が数学を説明する方法です。彼らは用語の定義を書き、それに基づいてルールを記述します。 このような仕様の利点は、850 行のコードよりも 850 つのルールの方が理解とデバッグがはるかに簡単であることです。 これらのルールを書くのは簡単ではなく、デバッグにはかなりの時間がかかりました。 特にこの目的のために、どのルールが使用されたかを報告するコードを書きました。 これら XNUMX つのルールをいくつかの例でテストしたおかげで、XNUMX 行のコードをデバッグする必要がなくなり、バグを見つけるのが非常に簡単になったことがわかりました。 Java にはこのための優れたツールがあります。 コードを書くだけだったら、もっと時間がかかり、フォーマットの品質も低かったでしょう。

なぜ正式な仕様を使用できなかったのでしょうか? 一方で、ここでは正しい実行はそれほど重要ではありません。 構造的なプリントアウトは誰にも喜ばれないはずなので、すべての奇妙な状況で正しく動作させる必要はありませんでした。 さらに重要なのは、適切なツールを持っていなかったという事実です。 ここでは TLA+ モデル チェッカーは役に立たないため、サンプルを手動で作成する必要があります。

上記の仕様には、すべての仕様に共通する特徴があります。 コードよりも高レベルです。 どの言語でも実装できます。 それを書くのにどんなツールや方法も役に立ちません。 この仕様を書くのに役立つプログラミングコースはありません。 そして、もちろん、TLA+ で構造化印刷プログラムを作成するための専用の言語を作成しない限り、この仕様を不要にするツールはありません。 最後に、この仕様では、コードを正確にどのように記述するかについては何も述べておらず、このコードが何を行うかについてのみ述べています。 コードについて考え始める前に、問題をじっくり考えるのに役立つ仕様を作成します。

ただし、この仕様には他の仕様とは異なる特徴もあります。 他の仕様の 95% は大幅に短く、よりシンプルです。

さらに、この仕様は一連のルールです。 一般に、これは仕様が不十分であることを示します。 一連のルールの結果を理解するのは非常に難しいため、ルールのデバッグに多くの時間を費やす必要がありました。 ただし、この場合、これより良い方法が見つかりませんでした。

継続的に実行されるプログラムについて少し述べておく価値があります。 原則として、これらは、オペレーティング システムや分散システムなどで並行して動作します。 それらを頭や机上で理解できる人はほとんどいません。私もその一人ではありませんが、かつては理解できました。 したがって、TLA + や PlusCal など、作業をチェックするツールが必要です。

コードが何をすべきかをすでに知っているのに、なぜ仕様を書く必要があるのでしょうか? 実際、私はそれを知っていると思っただけです。 さらに、仕様を使用すると、部外者がコードに介入して正確に何をするのかを理解する必要がなくなります。 私にはルールがあります。一般的なルールは存在すべきではありません。 もちろん、この規則には例外があります。これが私が従う唯一の一般的な規則です。コードの動作の仕様は、コードを使用するときに知っておく必要があるすべてのことをユーザーに伝える必要があります。

では、プログラマーは思考について正確に何を知っておく必要があるのでしょうか? まず、他の人たちと同じように、書かなければ、自分が考えているようにしか見えません。 また、コードを書く前に考える必要があります。つまり、コードを書く前に書く必要があります。 仕様はコーディングを開始する前に記述するものです。 誰でも使用または変更できるコードには仕様が必要です。 そして、この「誰か」は、コードが書かれてから XNUMX か月後のコードの作成者自身である可能性があります。 仕様は、大規模なプログラムやシステム、クラス、メソッド、さらには単一メソッドの複雑なセクションにも必要です。 コードについては具体的に何を書けばよいのでしょうか? それが何をするのか、つまり、このコードを使用する人にとって何が役立つのかを説明する必要があります。 場合によっては、コードがその目的を達成する方法を指定する必要がある場合もあります。 アルゴリズムの過程でこのメソッドを実行した場合、それをアルゴリズムと呼びます。 それがより特別で新しいものであれば、それをハイレベルデザインと呼びます。 ここには形式的な違いはありません。どちらもプログラムの抽象モデルです。

コード仕様は具体的にどのように書けばよいのでしょうか? 重要なことは、コード自体よりも XNUMX つ上のレベルである必要があることです。 状態と動作を説明する必要があります。 タスクに必要なだけ厳密である必要があります。 タスクの実装方法の仕様を作成する場合は、疑似コードまたは PlusCal を使用して作成できます。 正式な仕様書の書き方を学ぶ必要があります。 これにより、非公式なスキルでも役立つ必要なスキルが得られます。 正式な仕様の書き方をどのように学べますか? 私たちがプログラミングを学んだとき、私たちはプログラムを書いてそれをデバッグしました。 ここでも同じです。仕様を作成し、モデル チェッカーでチェックし、バグを修正します。 TLA+ は正式な仕様には最適な言語ではない可能性があり、特定のニーズには別の言語の方が適している可能性があります。 TLA+ の利点は、数学的思考を非常にうまく教えられることです。

仕様とコードをリンクするにはどうすればよいですか? 数学的概念とその実装を結び付けるコメントの助けを借りて。 グラフを操作する場合、プログラム レベルではノードの配列とリンクの配列が存在します。 したがって、これらのプログラミング構造によってグラフがどのように実装されるかを正確に記述する必要があります。

上記のいずれも、コードを記述する実際のプロセスには当てはまらないことに注意してください。 コードを書くとき、つまり XNUMX 番目のステップを実行するときも、プログラムを徹底的に考えて考える必要があります。 サブタスクが複雑または自明ではないことが判明した場合は、その仕様を記述する必要があります。 ただし、ここではコード自体について話しているのではありません。 あらゆるプログラミング言語、あらゆる方法論を使用できます。重要なのは、それらに関するものではありません。 また、上記のいずれによっても、コードのテストとデバッグが不要になります。 抽象モデルが正しく記述されていても、その実装にバグが存在する可能性があります。

仕様の作成は、コーディング プロセスの追加のステップです。 そのおかげで、より少ない労力で多くのエラーを検出できるようになります。これは、Amazon のプログラマーの経験からわかっています。 仕様があれば番組の質も高くなります。 では、なぜ私たちはそれらを使わずに過ごすことが多いのでしょうか? 書くのが大変だから。 そして、書くことは難しいです。なぜなら、そのためには考える必要があり、考えることも難しいからです。 自分の考えを偽るほうがずっと簡単です。 ここで、ランニングに例えることができます。走らないと、走る速度が遅くなります。 筋肉を鍛えて書く練習をする必要があります。 練習が必要です。

仕様が間違っている可能性があります。 どこかで間違いを犯したか、要件が変更されたか、あるいは改善が必要な可能性があります。 誰もが使用するコードは変更する必要があるため、遅かれ早かれ仕様はプログラムと一致しなくなります。 この場合、理想的には、新しい仕様を作成し、コードを完全に書き直す必要があります。 そんなことをする人はいないことを私たちはよく知っています。 実際には、コードにパッチを適用し、場合によっては仕様を更新します。 遅かれ早かれ必ずそうなるのであれば、なぜ仕様書を書く必要があるのでしょうか? まず、コードを編集する人にとって、仕様内のすべての余分な単語は金の価値があり、その人はおそらくあなた自身である可能性があります。 コードを編集するときに十分な仕様が得られていないと自分を責めることがよくあります。 そして、コードよりも仕様を書きます。 したがって、コードを編集する場合は、常に仕様を更新する必要があります。 第 XNUMX に、リビジョンが上がるたびにコードは悪化し、読み取りや保守がますます難しくなります。 これがエントロピーの増加です。 しかし、仕様から始めないと、書くすべての行が編集になり、コードは最初から扱いにくく、読みにくくなります。

言ったように アイゼンハワー, 計画によって勝利した戦いはなく、計画なしに勝利した戦闘もない。 そして彼は戦いについてある程度の知識を持っていました。 仕様書を書くのは時間の無駄だという意見があります。 場合によってはこれが真実であり、タスクは非常に単純であるため、じっくり考える必要はありません。 しかし、仕様書を書くなと言われるときは、考えるなと言われていることを常に覚えておく必要があります。 そして、毎回それについて考えるべきです。 タスクを徹底的に考えても、間違いを犯さないという保証はありません。 ご存知のとおり、魔法の杖を発明した人は誰もおらず、プログラミングは難しい作業です。 しかし、問題をよく考えなければ間違いを犯すことは間違いありません。

TLA + と PlusCal について詳しくは、特別な Web サイトをご覧ください。私のホームページからアクセスできます。 リンク。 以上でございます。ご清聴ありがとうございました。

これは翻訳であることに注意してください。 コメントを書くときは、投稿者がコメントを読むわけではないことに注意してください。 著者と本当に話したい場合は、2019 年 11 月 12 ～ 2019 日にサンクトペテルブルクで開催される Hydra XNUMX カンファレンスに彼が参加します。 チケットは購入できます 公式ウェブサイト上で.

出所： habr.com