1

X命令型コード（および周囲のプログラム）のチャンクが与えられた場合、そのコードが参照透過性であるかどうかを判断できるアルゴリズムはありますか？

私がこれまでに持っているのは：

コードの一部は、次の場合はRTです。

  1. 制御フローがXを離れた後、Xで割り当てられた非参照変数は読み取られません。

  2. 参照が解除され、Xで割り当てられているすべての参照変数は、ルール1に従って変数を参照していることを証明できます。

  3. scanf()変数が読み取られたり、関数が呼び出されたりすることはありません。その値は実行時の状態（つまり、、）に依存しますtime()。argv

編集：コメントを参照

このアルゴリズムの完全な精度は絶対に必要というわけではありませんが、望ましいです。（これは実際の生活であり、CSクラスではないので、ある人が「正しいよりも単純である方が少し良い」と言っています。）

編集2：

抽象構文木として表される、参照やポインターのない単純化された言語のアルゴリズムスケッチ/アイデア：

  1. 原因と結果のペアを見つける（つまり、変数の割り当てと使用）
  2. 各ペアについて、ASTの親ノードを、最も低い共通の祖先までの非RTとしてマークします。

問題：初期化子についてどうすればよいですか？それらは割り当てとしてカウントされますか？

4

2 に答える 2

2

2つのコードが一般的に参照透過性であるかどうかを判断することは可能ですか？いいえ、なぜですか？プログラム分析は完全に正確ではないため（証明：大量の異なる定式化、基本的に停止性問題）。ただし、概算することができます。一般に、どのタイプのプログラムが確実に参照透過性であるかを証明するためのいくつかの手法があります（近似の保守的な側面でエラーが発生するため、正しいが正しいことを示すことができないプログラムが必ず存在します）。

  • まず、言語を修正する必要があります。分析は言語に依存し、分析の複雑さは、言語に含まれるもの（並行性、参照、ポインターなど、すべて処理が難しいもの）に応じて大きく変化します。（参照とポインターは同じではありません。一般に、任意のポインター演算を処理することは、単純な参照よりも困難です！）
  • いくつかの定理証明者またはモデルチェッカーを見ることができます。これらのツールを使用すると、プログラムをモデル化する式を導出し、それらが同じ動作セットを記述しているかどうかを判断することにより、2つのプログラムの出力が同じかどうかを確認できます。
  • 分離ロジックは、ポインターが存在する場合に2つの命令型プログラムが正しいことを証明するために、非常に人気があり、成長している手法です。基本的な考え方は、ヒープの互いに素な部分について構成的に推論することです（なぜこれが良いのですか？リンクリストの実装を作成し、そのリンクリストの中央にランダムに書き込むコードと組み合わせます。これは検証の地獄です。 ）。
  • 機能の世界では、人々はコードに等式の推論を適用しようとします。これは命令型プログラムでは完全に同じではありませんが、モナドを使用してヒープアサーションをモデル化する場合は、同様のことを行うことができます。

大規模なコードベースにすぐに適用できるツールはありますか？いいえ、大規模なコードベースは推論に適さないものを使用しているためです（リフレクション、エイリアシングの難しいクラスなど）。基本的に、問題はある種の定理証明に還元されます。そこでは、2つのプログラムが同等であることを証明できる必要があります。サブ問題のためにこれに取り組むたくさんの論文があります。たとえば、おもちゃの言語で書かれた非常に単純なプログラムを考えてみましょう（Impは人気のある例です！）、たくさんの論文がこのようなことに取り組んでいます。

于 2012-09-19T01:11:42.373 に答える
2

計算にどのような副作用があるかを記述および追跡するためのメカニズムである「エフェクトシステム」または「タイプおよびエフェクトシステム」について読みたいと思うかもしれません。エフェクトアノテーションに頼るのではなく推論ができるシステムがあるかどうかはわかりませんが、少なくとも心配しなければならないことを理解できるはずです。

于 2012-09-18T20:14:19.593 に答える