機能的には同等だが意味的には異なるコンピュータ プログラムを生成するための理論的基礎を説明するドキュメントまたは特定のテキストはありますか? 理想的には、 KLEEと同じ流れで実際のプログラミング言語の個別の命令からシンボリック命令を導出する基礎をカバーするドキュメントを探しています。
2 つのコードが同等の連続した実行状態のサブセットを共有するかどうかを判断する際に、複雑さの下限があるかどうかも興味があります。
機能的には同等だが意味的には異なるコンピュータ プログラムを生成するための理論的基礎を説明するドキュメントまたは特定のテキストはありますか? 理想的には、 KLEEと同じ流れで実際のプログラミング言語の個別の命令からシンボリック命令を導出する基礎をカバーするドキュメントを探しています。
2 つのコードが同等の連続した実行状態のサブセットを共有するかどうかを判断する際に、複雑さの下限があるかどうかも興味があります。
最初の問題については、説明した機能のサブセットであるポリモーフィック コードの研究に興味があるかもしれません。
2 番目の問題の場合:
2 つのコードが機能的に同等であるかどうかを判断することは、よく知られている決定不能な問題である停止問題と同じくらい困難です。問題のすべてのインスタンスを解決できるコンピュータはありません。
それを確認するには、テストするプログラムが停止しないプログラムと同等の機能を持っているかどうかを尋ねることで、停止する問題を解決できることに注意してくださいfor(;;);
。私たちは副作用を無視しているので、その間にプログラムが何か他のことをするかどうかは気にしません。私たちが気にするのは、最終的に終了するかどうかだけです。