形式手法に関する論文で「ループを折りたたんで終了させる必要がある」(正確には抽象解釈)に出くわしました。終了の意味はわかりますが、折り畳まれたループとは何か、ループで折り畳みを実行する方法もわかりません。
誰かが私に折り畳まれたループが何であるかを説明してもらえますか?そして、それが暗黙的ではない場合、または折り畳まれたループの定義にすぐに従わない場合、これはどのように終了を保証しますか?
ありがとう
形式手法に関する論文で「ループを折りたたんで終了させる必要がある」(正確には抽象解釈)に出くわしました。終了の意味はわかりますが、折り畳まれたループとは何か、ループで折り畳みを実行する方法もわかりません。
誰かが私に折り畳まれたループが何であるかを説明してもらえますか?そして、それが暗黙的ではない場合、または折り畳まれたループの定義にすぐに従わない場合、これはどのように終了を保証しますか?
ありがとう
ループを折りたたむことは、よく知られているループ展開とは逆の動作であり、それ自体はループ展開としてよく知られています。ループが与えられた場合、展開するということは、本体を数回繰り返すことを意味するため、ループテストの実行頻度は低くなります。ループの実行回数が事前にある場合、ループを完全に展開して、単純な一連の命令を残すことができます。たとえば、このループ
for i := 1 to 4 do
writeln(i);
に展開することができます
writeln(1);
writeln(2);
writeln(3);
writeln(4);
部分的に展開する別の例については、C++ループの展開と境界を参照してください。
比喩は、プログラムが何度も折りたたまれているというものです。展開とは、これらの折り目の一部またはすべてを削除することを意味します。
一部の静的解析手法では、ループのエントリポイントの前提条件を見つける(つまり、ループ不変条件を見つける)には、一般に解決できない不動点の計算が必要になるため、ループを処理するのは困難です。したがって、一部の分析ではループが展開されます。これには、反復回数に合理的な制限が必要であり、分析できるプログラムの範囲が制限されます。
他の静的分析手法では、適切な不変条件を見つけることが分析の重要な部分です。ループを展開することは役に立ちません。実際、ループを部分的に展開すると、ループ本体が大きくなり、適切な不変条件を決定するのがより困難になります。反復回数が多いか無制限の場合、ループを完全に展開することは非現実的または不可能です。論文を見ずに、コードが展開された形式で記述されている可能性があるため、ステートメントは少し驚くべきものですが、分析がより折りたたまれた形式でのみ機能するプログラムが存在する可能性があります。
私は抽象解釈の知識がないので、関数型プログラミングのアプローチでフォールディングを行います。:-)
関数型プログラミングでは、フォールドはリストに適用される操作であり、各要素で何かを実行し、反復ごとに値を更新します。たとえば、次のように実装できますmap
(Schemeで)。
(define (map1 func lst)
(fold-right (lambda (elem result)
(cons (func elem) result))
'() lst))
それは、空のリストで始まり(結果と呼びましょう)、リストの各要素について、右側から左に移動func
して、要素とcons
その結果を結果リストに呼び出します。 。
ここで重要なのは、終了に関しては、リストが有限である限り、ループは確実に終了することです。これは、リストの次の要素を毎回反復しているためです。有限である場合、最終的に次の要素はありません。
これをfor
、リストでは機能せず、代わりにの形式を持つ、よりCスタイルのループと比較してくださいfor (init; test; update)
。はtest
falseを返すことが保証されていないため、ループが完了することは保証されていません。