コンピューター プログラムは、数学的なステートメントと同じように証明できないのはなぜですか? 数学的証明は、さらに多くの証明から構築された他の証明の上に構築され、公理に至るまでです。
コンピュータプログラムはそのような構造を持っていないようです。コンピューター プログラムを作成した場合、以前に証明された作品を使用して、プログラムの真実を示すことができるのはどうしてですか? 存在しないのでできません。さらに、プログラミングの公理とは何ですか? フィールドの非常に原子的な真実？
上記に対する良い答えはありません。しかし、ソフトウェアは科学ではなく芸術であるため、証明できないようです。ピカソであることをどのように証明しますか?
証明はプログラムです。
プログラムの正式な検証は、巨大な研究分野です。(たとえば、カーネギー メロン大学のグループを参照してください。)
多くの複雑なプログラムが検証されています。たとえば、Haskell で記述されたこのカーネルを参照してください(修復された 404 リンクはseL4用です。移動先の場所とプロジェクトの Web サイトも参照してください)。
プログラムが正しいことは絶対に証明できます。お粗末なプログラムを証明するのは困難です。それをかなりうまく行うには、プログラムを進化させて証明する必要があります。
停止問題のため、証明を自動化することはできません。ただし、任意のステートメントまたは一連のステートメントの事後条件と事前条件を手動で証明することはできます。
Dijsktra のA Discipline of Programming を読む必要があります。
次に、Gries のThe Science of Programming を読む必要があります。
そうすれば、プログラムが正しいことを証明する方法がわかります。
実際、あなたは確かに正しいプログラムを書くことができます。たとえば、Microsoftは、自動定理証明を含むSpec＃と呼ばれるC＃言語の拡張機能を作成しました。javaには、ESC/javaがあります。そこにはもっとたくさんの例があると確信しています。
（編集：どうやらspec＃はもう開発されていませんが、コントラクトツールは.NET 4.0の一部になります）
プログラムの自動検証を妨げると思われる停止性問題や不完全性定理について手を振っているポスターがいくつかあります。もちろん、これは真実ではありません。これらの問題は、正しいか間違っているかを証明できないプログラムを書くことが可能であることを示しているにすぎません。それは、私たちが確かに正しいプログラムを構築することを妨げるものではありません。
停止の問題は、検証できないプログラムがあることを示しているだけです。より興味深く、より実用的な問題は、どのクラスのプログラムを正式に検証できるかということです。おそらく、誰もが気にかけているすべてのプログラムを (理論的には) 検証することができます。 実際には、これまでのところ、非常に小さなプログラムのみが正しいことが証明されています。
不完全性を指摘した人へのちょっとしたコメントです。それはすべての公理システムに当てはまるわけではなく、十分に強力なシステムにのみ当てはまります。
言い換えれば、ゲーデルは、それ自体を説明するのに十分強力な公理系は必然的に不完全であることを証明しました。ただし、これは役に立たないという意味ではありません。他の人がリンクしているように、プログラムの証明に関するさまざまな試みが行われています。
二重問題 (証明をチェックするプログラムを書くこと) も非常に興味深いものです。
このトピックに本当に興味がある場合は、まず、このトピックに関する古典的な入門書である David Gries の「The Science of Programming」をお勧めします。
実際、プログラムが正しいことをある程度証明することは可能です。事前条件と事後条件を記述し、事前条件を満たしている状態が与えられた場合、実行後の結果の状態が事後条件を満たしていることを証明できます。
ただし、難しいのはループです。これらについては、さらにループ不変条件を見つける必要があり、正しい終了を示すために、各ループ後に残っている反復の最大可能回数の上限関数を見つける必要があります。また、ループを反復するたびに、これが少なくとも 1 ずつ減少することを示すことができなければなりません。
プログラムのこれらすべてがあれば、証明は機械的です。残念ながら、ループの不変関数と束縛関数を自動的に導出する方法はありません。小さなループの些細なケースでは人間の直感で十分ですが、現実的には、複雑なプログラムはすぐに手に負えなくなります。
まず、なぜ「プログラムは証明できない」と言っているのですか？
とにかく「プログラム」とはどういう意味ですか？
プログラムによってアルゴリズムを意味している場合、クラスカル法を知らないのですか？ダイクストラの？MST？プリム？二分探索？マージソート？DP？それらすべてのものには、それらの振る舞いを説明する数学的モデルがあります。
説明。数学は、物事の理由を説明するのではなく、単にその方法の絵を描くだけです。明日東に太陽が昇ることを証明することはできませんが、過去にそのことを行っていたデータを示すことはできます。
あなたは次のように述べています。「コンピュータプログラムを作成する場合、これまでに証明された作品をどのように使用して、プログラムの真実を示すことができますか？何も存在しないため、できません」
待って？できません？ http://en.wikipedia.org/wiki/Algorithm#Algorithmic_analysis
私はあなたに「真実」を示すことができません私はあなたに言語で「真実」を示すことができないのと同じくらい私はプログラムです。どちらも、私たちの世界に対する経験的理解を表しています。「真実」ではありません。すべてのぎこちなさはさておき、マージソートアルゴリズムがO（nlogn）パフォーマンスでリスト上の要素をソートすること、ダイクストラが加重グラフで最短経路を見つけること、またはユークリッドのアルゴリズムがあなたに最大を見つけることを数学的に示すことができます2つの数値間の共通除数。その最後の場合の「私のプログラムの真実」は、2つの数値の間で最大公約数を見つけることになるかもしれませんね。
漸化式を使用して、フィボナッチプログラムがどのように機能するかを説明できます。
さて、コンピュータプログラミングは芸術ですか？確かにそうだと思います。数学と同じくらい。
私は数学のバックグラウンドを持っていないので、無知を許してください。しかし、「プログラムを証明する」とはどういう意味ですか？何を証明していますか？正しさ？正しさは、プログラムが「正しい」ことを確認する必要がある仕様です。しかし、この仕様は人間によって決定されます。この仕様が正しいことをどのように確認しますか？
私の考えでは、人間は本当に欲しいものを表現するのが難しいため、プログラムにはバグがあります。 代替テキストhttp://www.processdevelopers.com/images/PM_Build_Swing.gif
それで、あなたは何を証明していますか？注意の欠如によって引き起こされたバグ？
さらに、プログラミングの公理とは何ですか? フィールドの非常に原子的な真実？
Contract Based Programming (コースのホームページ: http://www.daimi.au.dk/KBP2/ ) というコースを TA しました。ここで、コース（および私が受講した他のコース）から推測できること
言語のセマンティクスを形式的に (数学的に) 定義する必要があります。簡単なプログラミング言語を考えてみましょう。グローバル変数のみ、int、int 配列、算術、if-then-else、while、代入、および何もしないもの [これの「実装」として、主流の言語のサブセットをおそらく使用できます]。
実行状態は、ペア (変数名、変数の値) のリストになります。「{Q1} S1 {Q2}」を「ステートメント S1 を実行すると、実行状態 Q1 から状態 Q2 に移行する」と読みます。
1 つの公理は になります"if both {Q1} S1 {Q2} and {Q2} S2 {Q3}, then {Q1} S1; S2 {Q3}"。つまり、ステートメント S1 で状態 Q1 から Q2 に移動し、ステートメント S2 で Q2 から Q3 に移動した場合、"S1; S2" (S1 の後に S2 が続く) で状態 Q1 から状態 Q3 に移動します。
別の公理は です"if {Q1 && e != 0} S1 {Q2} and {Q1 && e == 0} S2 {Q2}, then {Q1} if e then S1 else S2 {Q2}"。
ここで、少し改良します。{} 内の Qn は、実際には状態そのものではなく、状態に関するステートメントになります。
M(out, A1, A2) が、ソートされた 2 つの配列をマージして結果を out に格納するステートメントであり、次の例で使用するすべての単語が形式的に (数学的に) 表現されているとします。次に"{sorted(A1) && sorted(A2)} A := M(A1, A2) {sorted(A) && permutationOf(A, A1 concatened with A2)}"、M がマージ アルゴリズムを正しく実装しているという主張です。
上記の公理を使用して、これを証明しようとすることができます (他にもいくつかの公理が必要になる可能性があります。たとえば、ループが必要になる可能性があります)。
これが、プログラムが正しいことを証明することがどのように見えるかを少し示してくれることを願っています. そして、私を信じてください。一見単純なアルゴリズムであっても、それらが正しいことを証明するには多くの作業が必要です。私は知っています、私は多くの試みを読みました;-)
[これを読んだ場合:あなたのハンドインは問題ありませんでした。頭痛の種は他のすべてのハンドインです ;-)]
もちろん、他の人が投稿したように、それらは可能です。
非常に小さなサブルーチンが正しいことを証明することは、プログラミング関連の学位プログラムのすべての学部生が行う必要がある良い練習です。コードを明確にし、レビューしやすく、保守しやすいものにする方法を考える上で、大きな洞察を与えてくれます。
ただし、現実の世界では、実用的な用途は限られています。
まず、プログラムにバグがあるように、数学的な証明にもバグがあります。数学的な証明が本当に正しく、誤りがないことをどのように証明しますか? できません。そして反例として、出版された数学的証明の多くは、時には何年も後に誤りを発見しました。
第 2 に、プログラムが何をすべきかについて「先験的に」明確な定義がなければ、プログラムが正しいことを証明することはできません。しかし、プログラムが何をすべきかについての明確な定義はすべてプログラムです。(コンパイラを持っていないある種の仕様言語のプログラムかもしれませんが。) したがって、プログラムが正しいことを証明する前に、同等で事前にわかっている別のプログラムを用意する必要があります。正しいこと。したがって、QED全体が無駄です。
Brooks による古典的な記事「 No Silver Bullet 」をたどることをお勧めします。
彼らはできます。私は大学の新入生として、プログラムの正当性の証明を行うために何時間も費やしました。
マクロスケールで実用的でない理由は、プログラムの証明を書くことは、プログラムを書くことよりもはるかに難しい傾向があるためです。また、今日のプログラマーは、関数やプログラムを作成するのではなく、システムを構築する傾向があります。
マイクロスケールでは、個々の関数に対して精神的に行うことがあり、コードを整理して検証しやすくする傾向があります。
スペースシャトルソフトウェアについての有名な記事があります。彼らは証明、または同等のものを行います。それは信じられないほど費用と時間がかかります。そのレベルの検証が必要な場合もありますが、現在の技術を使用しているあらゆる種類の消費者向けまたは商用ソフトウェア会社では、1％のコストで99.9％のソリューションを提供する競合他社に昼食を食べさせます。わずかに安定しているMSOfficeに5000ドルを支払う人は誰もいません。
自信を求めている場合、プログラムを証明する代わりに、プログラムをテストします。これは理解しやすく、自動化できます。また、上記のように、証明が数学的に不可能なクラスのプログラムも考慮に入れます。
何よりも、受け入れテストに合格することの代わりになる証拠はありません:*
プログラムが言うことを実際に実行するからといって、ユーザーが実行したいことを実行するとは限りません。
それが言っていることがユーザーが望んでいると言っていることを証明できない限り。
*ユニット、カバレッジ、機能、統合、その他すべての種類のテストは言うまでもありません。
これがあなたの道に役立つことを願っています。
プログラムを証明できるだけでなく、コンピュータに証明からプログラムを構築させることもできます。Coqを参照してください。したがって、実装でミスを犯した可能性について心配する必要さえありません。
この分野では多くの研究が行われています.他の人が言ったように、プログラム言語内の構造は複雑であり、与えられた入力を検証または証明しようとすると、これは悪化するだけです.
ただし、多くの言語では、どの入力が受け入れられるか (前提条件) を指定でき、最終結果 (事後条件) を指定することもできます。
そのような言語には、B、Event B、Ada、fortran などがあります。
そしてもちろん、プログラムに関する特定の特性を証明するのに役立つように設計された多くのツールがあります。たとえば、デッドロックの自由を証明するために、SPIN を使用してプログラムをクランチできます。
また、論理エラーの検出に役立つツールも数多くあります。これは、静的分析 (goanna、stabs) またはコードの実際の実行 (gnu valgrind?) によって行うことができます。
ただし、開始 (仕様)、実装、展開から、プログラム全体を実際に証明できるツールはありません。B メソッドはそれに近づきますが、その実装チェックは非常に弱いものです。(それは、スペシフィケーションから実装への変換において、人間は間違いないと仮定しています)。
補足として、B メソッドを使用すると、小さな公理から複雑な証明を作成することがよくあります。(そして、同じことが他の網羅的定理証明者にも当てはまります)。
ここで言及されていないのは、正式な方法ベースのシステムであるB - メソッドです。パリの地下鉄の安全システムの開発に使用されました。B および Event B の開発をサポートするために利用できるツールがあり、特にRodinがあります。
プログラムは証明できます。たとえば、ニュージャージーの標準 ML (SML/NJ) のような言語で記述すれば、非常に簡単です。
純粋関数型言語 (つまり Haskell) を想定してみましょう。そのような言語では、副作用を非常に明確に考慮することができます。
プログラムが正しい結果を生成することを証明するには、以下を指定する必要があります。
この一連の仕様は、表示セマンティクスと呼ばれます。それらは、数学を使用してプログラムについての理由を証明することを可能にします。
良いニュースは、「プログラムの構造」(上記のポイント 3) と「数学的集合の構造」が非常に似ていることです (流行語はtopos、またはデカルトの閉じたカテゴリです)。したがって、1/ 数学側で行う証明は2/ あなたが書いたプログラムは、数学的に正しいことが容易に示されます。
あなたの発言は広いので、たくさんの魚を捕まえています。
結論としては、一部のプログラムは間違いなく正しいことが証明できるということです。すべてのプログラムが正しいと証明できるわけではありません。
これは、当時集合論を破壊したのとまったく同じ種類の証明である、些細な例です: それ自体が正しいかどうかを判断できるプログラムを作成し、それが正しいことがわかった場合は、間違った答えを返します。
これは単純明快なゲーデルの定理です。
しかし、多くのプログラムを証明できるので、これはそれほど問題ではありません。
ゲーデルの定理にもかかわらず...何がポイントになるのでしょうか? どのような単純な「真実」を証明したいですか? それらの真実から何を導き出したいですか？私はこれらの言葉を食べるかもしれませんが...実用性はどこにありますか？
あまり抽象的な観点からは、何かを証明することは、不確実性の分野を証明されたヌルセットに減らすことの問題です。現実の世界では完璧に到達できないので、それは希望に満ちた考えです。
コンピュータプログラムは、その環境が証明されていない（または証明できない）場合、確かに正しく、現実の世界では失敗する可能性があります。
OSカーネル、ドライバー、すべてのユーザーモードライブラリ、および同時に実行されるプログラムは、直接的および間接的な短期的および長期的な副作用を含めて、証明する必要があります。
ハードウェアは常に期待どおりに動作する必要があります（停電、洪水、地震、EMF干渉などを含む）。
エンドユーザーは常に期待どおりに動作する必要があります（有名な要素「X」）。
自動エラー訂正は、さまざまなハードウェアコンポーネント（RAM、ディスク、コントローラーなど）に実装されていますが、それでもハードウェア障害が発生し、カスケードエラーや...provably correctプログラムの障害が発生します。
そして、私はエンドユーザーの創造性についてエピローグしようとさえしていません...
したがって、（正しく）評価されたプログラムは、それが実際にprovably correct存在することを意味するものではありません。provably safe
これは、定義された調査で検討されたセット（実世界のサブセットにしかなり得ない）の場合、このプログラムは期待どおりに動作することを意味します。
ここは騒がしいけど、とにかく風になびいて叫ぶよ...
「正しいことを証明する」は、文脈によって意味が異なります。正式なシステムでは、「正しいことを証明する」とは、ある式が他の証明された (または公理的な) 式から導出できることを意味します。プログラミングにおける「正しい証明」は、コードが正式な仕様と同等であることを示すだけです。しかし、正式な仕様が正しいことをどのように証明しますか? 残念ながら、仕様にバグがないことや、実際の問題を解決できることを示す方法は、テスト以外にはありません。
ちょうど私の 2 セント、既にそこにある興味深いものに追加します。
Of all the programs that can't be proven, the most common ones are those performing IO (some unpredictible interaction with the world or the users). Even automated proofs sometimes just forget that "proven" programs" run on some physical hardware, not the ideal one described by the model.
On the other side mathematic proofs don't care much of the world. A recurring question with Maths is if it describes anything real. It is raised every time something new like imaginary numbers or non-euclidian space is invented. Then the question is forgotten as these new theories are such good tools. Like a good program, it just works.
これについて少し読みましたが、2つの問題があります。
まず、正当性と呼ばれる抽象的なものを証明することはできません。適切に設定されていれば、2 つの正式なシステムが同等であることを証明できます。プログラムが一連の仕様を実装していることを証明できます。これを行うには、証明とプログラムを多かれ少なかれ並行して構築するのが最も簡単です。したがって、仕様は、証明するものを提供するために十分に詳細である必要があり、したがって、仕様は実質的にプログラムです。目的を満たすためにプログラムを書く問題は、目的を満たすためにプログラムの正式な詳細仕様を書く問題になり、それは必ずしも一歩前進ではありません。
第二に、プログラムは複雑です。正しさの証明も同様です。プログラムを書いて間違いを犯すことができるなら、間違いなく証明することができます。Dijkstra と Gries は、基本的に、私が完璧な数学者であれば、優れたプログラマーになれるだろうと言っていました。ここでの価値は、証明とプログラミングは 2 つの多少異なる思考プロセスであり、少なくとも私の経験では、さまざまな種類の間違いを犯すことです。
私の経験では、プログラムを証明することは役に立たないわけではありません。正式に説明できることをしようとしているとき、実装が正しいことを証明することで、見つけにくいエラーが大量に排除され、主に愚かなエラーが残り、テストで簡単に見つけることができます。非常にバグのないコードを生成する必要があるプロジェクトでは、便利な付属物になる可能性があります。すべてのアプリケーションに適しているわけではなく、特効薬ではないことは確かです。
プログラムが正しいことを証明することは、プログラムの仕様に関連してのみ行うことができます。可能ですが、費用と時間がかかります
一部のCASEシステムは、他のシステムよりも証明に適したプログラムを生成しますが、これも仕様の正式なセマンティクスに依存しています...
...では、仕様が正しいことをどのように証明しますか? 右！さらにスペックアップ！
他の人が指摘したように、(いくつかの) プログラムは実際に証明できます。
ただし、実際の問題の 1 つは、最初に証明したいもの(つまり、仮定または定理) が必要になることです。したがって、プログラムについて何かを証明するには、最初にそれが何をすべきかの正式な説明が必要です (たとえば、事前条件と事後条件)。
つまり、プログラムの正式な仕様が必要です。しかし、合理的な (厳密な形式ではなく) 仕様を取得することは、ソフトウェア開発においてすでに最も困難なことの 1 つです。したがって、(現実世界の) プログラムについて興味深いことを証明することは一般的に非常に困難です。
ただし、より簡単に形式化 (および証明) できる (および形式化されている) ものもいくつかあります。少なくともプログラムがクラッシュしないことを証明できれば、それはすでに何かです:-)。
ところで、一部のコンパイラの警告/エラーは、本質的にプログラムに関する (単純な) 証拠です。たとえば、Java コンパイラは、コード内の初期化されていない変数にアクセスしないことを証明します (そうしないと、コンパイラ エラーが発生します)。
停止問題(これは、プログラムが完了するかどうかという単純なことを証明することの難しさに関するものです)を読んでください。基本的に、この問題はゲーデルの不完全性定理に関連しています。
プログラムの一部は証明できます。たとえば、コンパイルが成功した場合に型の安全性を静的に検証して保証する C# コンパイラ。しかし、あなたの質問の核心は、プログラムが正しく動作することを証明することだと思います。多くの (ほとんどとは言いません) アルゴリズムが正しいことを証明できますが、次の理由により、プログラム全体を静的に証明することはおそらくできません。
そして、それらはほんの一部です...
さらに、プログラミングの公理とは何ですか? フィールドの非常に原子的な真実？
オペコードは「原子の真実」ですか？たとえば、見て...
mov ax,1
... プログラマーは、ハードウェアの問題がなければ、このステートメントを実行した後、CPU のaxレジスターに1.
コンピューター プログラムを作成した場合、以前に証明された作品を使用して、プログラムの真実を示すことができるのはどうしてですか?
「以前の作業」は、新しいプログラムが実行されるランタイム環境である可能性があります。
新しいプログラムは証明することができます: 正式な証明とは別に、「検査によって」およびさまざまな形式の「テスト」(「受け入れテスト」を含む) によって証明することができます。
ピカソであることをどのように証明しますか?
ソフトウェアがアートよりも工業デザインやエンジニアリングに近い場合、「橋や飛行機をどのように証明しますか?」という質問の方が適切かもしれません。
プログラムが明確に定義された目的と初期の仮定 (ゲーデルを無視して...) を持っている場合、それは証明できます。6<=x<=10 についてすべての素数 x を見つけます。答えは 7 であり、証明できます。私はNIM を実行するプログラム(私が書いた最初の Python プログラム) を書きましたが、理論的には、ゲームがコンピューターが勝てる状態になった後は常にコンピューターが勝ちます。私はそれが真実であることを証明できませんでしたが、コードに誤りがない限り、それは真実であると信じています (デジタル バイナリ合計証明による数学的に)。私は間違いを犯しましたか?
四色定理のように、コンピュータ コードで「証明」された数学的定理がいくつかあります。しかし、あなたが言ったように、プログラムを証明できますか?