私は自分のコンピューターで実行しているプログラムがクラッシュするかどうかを判断できるはずのプログラムに取り組んでいます。
おそらく、マシンコードを読み込み、潜在的なコードパスのモデルを構築し、標準および境界条件での動作について各コードパスをテストし、未処理の例外が発生する条件をマップしてから、これらすべてのステップを逆方向にトレースして生成することが可能です。例外的なコードパスをトリガーするために必要なセットアップ入力と条件。これは、ファジングデバッガーを使用するようなものですが、より系統だったものです。確かにそれは大変な作業ですが、最新のハードウェアでは非常に迅速に実行されるはずです。
同僚は、私がやろうとしていることは基本的に不可能だと言いました。それは私には少し極端に思えます。ムーアの技術開発の法則を考えると、手の届かないコンピューティング能力は最終的には現実のものになります-最終的には。そのようなことは永遠に不可能であり続けるだろうと示唆するのは少し誇張されているように思われるでしょう。
なぜこれができないのですか？
ここにプログラムがあります：
accept integer i greater than 2
loop with k from 2 to 2*i
is k prime?
is 2*i-k prime?
exit safely
end loop
do something nasty.
このプログラムが何か厄介なことをする原因となった入力をたどれば、ゴールドバッハの予想が解決されたことになります。ノーベル賞と一緒にフィールズメダルを集めることができます。
とはいえ、一部のプログラムが何も悪いことをしないことを確認することは可能です。私と他の人は、さまざまな手法を使用して、まさにそれを行うことができるフレームワークに取り組んでいます. いくつかの例：
この圧縮ライブラリでは、入力サイズ 20、出力サイズ 40 でメモリ エラーが発生する可能性がありましたが、現在は発生しません。
これは、 Entscheidungsproblemとして知られる、コンピューティングと数学の聖杯の 1 つです。あなたはそれを解決するつもりはありません。両方の分野の最も優秀な頭脳が何年も費やして、解決できないことを証明しました。nbt と Pascal Cuoq が、そうすればノーベル賞とフィールズ賞を受賞できると言ったとき、彼らは本当にそれを意味していました。
おそらく、マシン コードを読み取り、潜在的なコード パスのモデルを構築し、標準および境界条件下での動作について各コード パスをテストし、未処理の例外が発生する条件をマッピングし、それらすべての手順をさかのぼって生成することが可能です。必要なセットアップ入力と、例外的なコード パスの実行をトリガーする条件。
はい、理論の人々が何を言おうと、それは可能です。Vericode、Coverity、Fortify、Klocwork、Grammatech など、あなたが説明していることを正確に実行する製品を販売している会社は複数あります。
健全で完全な何かが欲しいと仮定すると、これは不可能であるという理論があります。実際には、偽陽性率がそれほど悪くない限り、健全性と完全性の両方を落とすことができ、顧客が製品を購入するために並んでいます.
健全性と完全性を落とすと、不可能性定理は成り立たなくなり、理論というよりもエンジニアリングに近いものになります。
編集、アレックスのコメントのために
、私は数学者の近道を取り、元の質問は「可能ですか」であるため、いくつかの実行可能な商用製品の存在は答えが「はい」であることを証明します. 商用ソフトウェアを使用することによって作成される可能性のある経済的な依存関係は、元の質問の範囲を超えています。