(57)【要約】【課題】任意の種類のデータ構造を対象としてデータ構造の形状の量的な変化を捉える。【解決手段】プログラム解析装置１０では、制御フローグラフ生成部１２が、プログラム記憶部１１に記憶されたプログラムから制御フローグラフを生成して制御フローグラフ記憶部１３に記憶し、初期マップ生成部１４が、プログラムの実行前におけるデータ構造の形状を表す形状グラフとそのデータ構造に含まれるオブジェクトの数との対応情報をマップ記憶部１５に記憶し、データフロー方程式生成部１６が、制御フローグラフ記憶部１３に記憶された制御フローグラフからデータフロー方程式を生成してデータフロー方程式記憶部１７に記憶し、マップ更新部１８が、データフロー方程式記憶部１７に記憶されたデータフロー方程式に基づいて、マップ記憶部１５に記憶された対応情報を更新する。【選択図】図３
2010020558.tif 000002
【特許請求の範囲】
【請求項１】
プログラムの処理対象であるデータ構造の形状を、当該形状を抽象的に表す形状グラフを用いて解析する装置であって、
前記プログラムの実行前における前記データ構造の形状を表す形状グラフと、当該データ構造に含まれるオブジェクトの数を表す標識との第１の対応情報を記録する第１の記録部と、
前記プログラムの実行後における前記データ構造の形状を表す形状グラフと、当該データ構造に含まれるオブジェクトの数を表す標識との第２の対応情報を記録する第２の記録部と、
前記第１の記録部により記録された前記第１の対応情報に含まれる標識と、前記第２の記録部により記録された前記第２の対応情報に含まれる標識とに基づいて、前記データ構造に含まれるオブジェクトの数の増減に関する情報を出力する出力部と
を備えた、装置。
【請求項２】
前記プログラムに含まれるステートメントを取得する取得部を更に備え、
前記第２の記録部は、前記取得部により前記ステートメントが取得される都度、当該ステートメントの実行後における前記データ構造の形状を表す形状グラフと、当該データ構造に含まれるオブジェクトの数を表す標識との対応情報を記録する処理を、当該対応情報が変化しなくなるまで行った結果として、前記第２の対応情報を記録する、請求項１の装置。
【請求項３】
前記第２の記録部は、前記対応情報を記録する処理において、前記取得部により取得された前記ステートメントが第１のデータ構造と第２のデータ構造とを連結する命令であることを条件の一つとして、当該ステートメントの実行前における当該第１のデータ構造に含まれるオブジェクトの数と当該ステートメントの実行前における当該第２のデータ構造に含まれるオブジェクトの数との和を表す標識を記録する、請求項２の装置。
【請求項４】
前記第２の記録部は、前記対応情報を記録する処理において、前記取得部により取得された前記ステートメントが前記データ構造に含まれる特定のオブジェクトを前記プログラムから到達できなくする命令であることを条件の一つとして、当該ステートメントの実行前における当該データ構造に含まれるオブジェクトの数から当該特定のオブジェクトの数を減じた値を表す標識を記録する、請求項２の装置。
【請求項５】
前記第２の記録部は、前記対応情報を記録する処理において、前記取得部により取得された前記ステートメントが前記データ構造に含まれる特定のオブジェクトを前記プログラムから到達できなくする命令であり、当該特定のオブジェクトの数を把握できない場合に、当該ステートメントの実行後における当該データ構造に含まれるオブジェクトの数が不明であることを表す標識を記録する、請求項２の装置。
【請求項６】
前記プログラムに含まれるステートメントを取得する取得部を更に備え、
前記第２の記録部は、前記取得部による第１のステートメントの取得に応じ、当該第１のステートメントに後続する第２のステートメントに入力される前記データ構造に関する情報として、当該第１のステートメントの実行後における前記データ構造の形状を表す形状グラフと、当該データ構造に含まれるオブジェクトの数を表す標識との第３の対応情報、及び、当該第２のステートメントに先行し、当該第１のステートメントとは異なる第３のステートメントの実行後における前記データ構造の形状を表す形状グラフと、当該データ構造に含まれるオブジェクトの数を表す標識との第４の対応情報を記録する、請求項１の装置。
【請求項７】
前記第２の記録部は、前記第３の対応情報に含まれる特定の形状グラフに対応する標識が、前記第４の対応情報に含まれる当該特定の形状グラフに対応する標識と異なることを条件の一つとして、当該特定の形状グラフと、前記データ構造に含まれるオブジェクトの数が不明であることを表す標識との対応情報を更に記録する、請求項６の装置。
【請求項８】
前記第２の記録部は、前記第３の対応情報に含まれる特定の形状グラフに対応する標識が、前記第４の対応情報に含まれる当該特定の形状グラフに対応する標識と異なり、これら２つの標識の差分が定数である場合に、当該特定の形状グラフと、当該２つの標識の一方の標識が表す値以上で他方の標識が表す値以下の値を表す標識との対応情報を更に記録する、請求項６の装置。
【請求項９】
プログラムの処理対象であるデータ構造の形状を、当該形状を抽象的に表す形状グラフを用いて解析する装置であって、
前記プログラムの実行前における前記データ構造の形状を表す形状グラフと、当該データ構造に含まれるオブジェクトの数を表す標識との第１の対応情報を記録する第１の記録部と、
前記プログラムに含まれるステートメントを取得する取得部と、
前記取得部により前記ステートメントが取得される都度、当該ステートメントの実行後における前記データ構造の形状を表す形状グラフと、当該データ構造に含まれるオブジェクトの数を表す標識との対応情報を記録する処理を、当該対応情報が変化しなくなるまで行うことにより、前記プログラムの実行後における前記データ構造の形状を表す形状グラフと、当該データ構造に含まれるオブジェクトの数を表す標識との第２の対応情報を記録する第２の記録部と、
前記第１の記録部により記録された前記第１の対応情報に含まれる標識と、前記第２の記録部により記録された前記第２の対応情報に含まれる標識とに基づいて、前記データ構造に含まれるオブジェクトの数の増減に関する情報を出力する出力部と
を備えた、装置。
【請求項１０】
プログラムの処理対象であるデータ構造の形状を、当該形状を抽象的に表す形状グラフを用いて解析する方法であって、
前記プログラムの実行前における前記データ構造の形状を表す形状グラフと、当該データ構造に含まれるオブジェクトの数を表す標識との第１の対応情報を記憶装置に記憶するステップと、
前記プログラムの実行後における前記データ構造の形状を表す形状グラフと、当該データ構造に含まれるオブジェクトの数を表す標識との第２の対応情報を前記記憶装置に記憶するステップと、
前記記憶装置に記憶された前記第１の対応情報に含まれる標識と、前記記憶装置に記憶された前記第２の対応情報に含まれる標識とに基づいて、前記データ構造に含まれるオブジェクトの数の増減に関する情報を出力するステップと
を含む、方法。
【請求項１１】
プログラムの処理対象であるデータ構造の形状を、当該形状を抽象的に表す形状グラフを用いて解析する装置としてコンピュータを機能させるプログラムであって、
前記コンピュータを、
前記プログラムの実行前における前記データ構造の形状を表す形状グラフと、当該データ構造に含まれるオブジェクトの数を表す標識との第１の対応情報を記録する第１の記録部と、
前記プログラムの実行後における前記データ構造の形状を表す形状グラフと、当該データ構造に含まれるオブジェクトの数を表す標識との第２の対応情報を記録する第２の記録部と、
前記第１の記録部により記録された前記第１の対応情報に含まれる標識と、前記第２の記録部により記録された前記第２の対応情報に含まれる標識とに基づいて、前記データ構造に含まれるオブジェクトの数の増減に関する情報を出力する出力部と
して機能させる、プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、データ構造の形状を解析する装置及び方法に関する。特に、本発明は、プログラムの処理対象であるデータ構造の形状を、その形状を抽象的に表す形状グラフを用いて解析する装置及び方法に関する。
【背景技術】
【０００２】
プログラムが用いるヒープ上のメモリにおいて、プログラムによって操作されるデータ構造がどのような形状をしているかを解析する形状解析と呼ばれる技術がある（例えば、非特許文献１参照）。この非特許文献１では、プログラム中の変数から直接指されないオブジェクトを１つのノードで抽象化した静的形状グラフを用いて形状解析を行っている。例えばデータ構造としてリストを考えた場合、その長さには無限の可能性があるが、非特許文献１では、この無限の可能性を有限の表現で解析することができる。
一方で、リストを操作するプログラムからカウンタオートマトンを作成する方法は既に提案されている（例えば、非特許文献２参照）。非特許文献２では、リストに対象を絞って、操作的意味等を定義し、そこからカウンタの更新等を定義している。
【０００３】
【非特許文献１】Sagiv, M. et al, “Solving Shape-Analysis Problems in Languages with Destructive Updating”， TOPLAS, Volume 20, Issue 1, January 1998, p.1-50
【非特許文献２】Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T., “Programs with Lists Are Counter Automata”, Computer Aided Verification 2006, Springer Berlin / Heidelberg, p.517-531
【発明の開示】
【発明が解決しようとする課題】
【０００４】
しかしながら、非特許文献１では、プログラム中の変数から直接指されないオブジェクトを１つのノードで抽象化しているので、オブジェクトの個数に関する情報は失われている。そのため、プログラムの実行の前後での形状の質的な変化を調べるには有用であるが、量的な変化を捉えることはできなかった。例えば、リストへ要素を挿入した結果もリストであることは示せるが、リストの長さに増減があったのかは分からなかった。
一方、非特許文献２では、リストに対象を絞って量的な変化を把握しており、限られたデータ型にしか対応できない。即ち、任意のデータ型を対象として形状の量的な変化を捉えることはできないという問題点があった。
【０００５】
本発明の目的は、任意の種類のデータ構造を対象としてデータ構造の形状の量的な変化を捉えることある。
【課題を解決するための手段】
【０００６】
かかる目的のもと、本発明は、プログラムの処理対象であるデータ構造の形状を、形状を抽象的に表す形状グラフを用いて解析する装置であって、プログラムの実行前におけるデータ構造の形状を表す形状グラフと、データ構造に含まれるオブジェクトの数を表す標識との第１の対応情報を記録する第１の記録部と、プログラムの実行後におけるデータ構造の形状を表す形状グラフと、データ構造に含まれるオブジェクトの数を表す標識との第２の対応情報を記録する第２の記録部と、第１の記録部により記録された第１の対応情報に含まれる標識と、第２の記録部により記録された第２の対応情報に含まれる標識とに基づいて、データ構造に含まれるオブジェクトの数の増減に関する情報を出力する出力部とを備えた、装置を提供する。
【０００７】
ここで、この装置は、プログラムに含まれるステートメントを取得する取得部を更に備え、第２の記録部は、取得部によりステートメントが取得される都度、ステートメントの実行後におけるデータ構造の形状を表す形状グラフと、データ構造に含まれるオブジェクトの数を表す標識との対応情報を記録する処理を、対応情報が変化しなくなるまで行った結果として、第２の対応情報を記録する、ものであってよい。
【０００８】
その際、第２の記録部は、対応情報を記録する処理において、取得部により取得されたステートメントが第１のデータ構造と第２のデータ構造とを連結する命令であることを条件の一つとして、ステートメントの実行前における第１のデータ構造に含まれるオブジェクトの数とステートメントの実行前における第２のデータ構造に含まれるオブジェクトの数との和を表す標識を記録する、ものであってよい。
また、第２の記録部は、対応情報を記録する処理において、取得部により取得されたステートメントがデータ構造に含まれる特定のオブジェクトをプログラムから到達できなくする命令であることを条件の一つとして、ステートメントの実行前におけるデータ構造に含まれるオブジェクトの数から特定のオブジェクトの数を減じた値を表す標識を記録する、ものであってよい。
更に、第２の記録部は、対応情報を記録する処理において、取得部により取得されたステートメントがデータ構造に含まれる特定のオブジェクトをプログラムから到達できなくする命令であり、特定のオブジェクトの数を把握できない場合に、ステートメントの実行後におけるデータ構造に含まれるオブジェクトの数が不明であることを表す標識を記録する、ものであってよい。
【０００９】
また、この装置は、プログラムに含まれるステートメントを取得する取得部を更に備え、第２の記録部は、取得部による第１のステートメントの取得に応じ、第１のステートメントに後続する第２のステートメントに入力されるデータ構造に関する情報として、第１のステートメントの実行後におけるデータ構造の形状を表す形状グラフと、データ構造に含まれるオブジェクトの数を表す標識との第３の対応情報、及び、第２のステートメントに先行し、第１のステートメントとは異なる第３のステートメントの実行後におけるデータ構造の形状を表す形状グラフと、データ構造に含まれるオブジェクトの数を表す標識との第４の対応情報を記録する、ものであってよい。
【００１０】
その際、第２の記録部は、第３の対応情報に含まれる特定の形状グラフに対応する標識が、第４の対応情報に含まれる特定の形状グラフに対応する標識と異なることを条件の一つとして、特定の形状グラフと、データ構造に含まれるオブジェクトの数が不明であることを表す標識との対応情報を更に記録する、ものであってよい。
また、第２の記録部は、第３の対応情報に含まれる特定の形状グラフに対応する標識が、第４の対応情報に含まれる特定の形状グラフに対応する標識と異なり、これら２つの標識の差分が定数である場合に、特定の形状グラフと、２つの標識の一方の標識が表す値以上で他方の標識が表す値以下の値を表す標識との対応情報を更に記録する、ものであってよい。
【００１１】
また、本発明は、プログラムの処理対象であるデータ構造の形状を、形状を抽象的に表す形状グラフを用いて解析する装置であって、プログラムの実行前におけるデータ構造の形状を表す形状グラフと、データ構造に含まれるオブジェクトの数を表す標識との第１の対応情報を記録する第１の記録部と、プログラムに含まれるステートメントを取得する取得部と、取得部によりステートメントが取得される都度、ステートメントの実行後におけるデータ構造の形状を表す形状グラフと、データ構造に含まれるオブジェクトの数を表す標識との対応情報を記録する処理を、対応情報が変化しなくなるまで行うことにより、プログラムの実行後におけるデータ構造の形状を表す形状グラフと、データ構造に含まれるオブジェクトの数を表す標識との第２の対応情報を記録する第２の記録部と、第１の記録部により記録された第１の対応情報に含まれる標識と、第２の記録部により記録された第２の対応情報に含まれる標識とに基づいて、データ構造に含まれるオブジェクトの数の増減に関する情報を出力する出力部とを備えた、装置も提供する。
【００１２】
更に、本発明は、プログラムの処理対象であるデータ構造の形状を、形状を抽象的に表す形状グラフを用いて解析する方法であって、プログラムの実行前におけるデータ構造の形状を表す形状グラフと、データ構造に含まれるオブジェクトの数を表す標識との第１の対応情報を記憶装置に記憶するステップと、プログラムの実行後におけるデータ構造の形状を表す形状グラフと、データ構造に含まれるオブジェクトの数を表す標識との第２の対応情報を記憶装置に記憶するステップと、記憶装置に記憶された第１の対応情報に含まれる標識と、記憶装置に記憶された第２の対応情報に含まれる標識とに基づいて、データ構造に含まれるオブジェクトの数の増減に関する情報を出力するステップとを含む、方法も提供する。
【００１３】
更にまた、本発明は、プログラムの処理対象であるデータ構造の形状を、形状を抽象的に表す形状グラフを用いて解析する装置としてコンピュータを機能させるプログラムであって、コンピュータを、プログラムの実行前におけるデータ構造の形状を表す形状グラフと、データ構造に含まれるオブジェクトの数を表す標識との第１の対応情報を記録する第１の記録部と、プログラムの実行後におけるデータ構造の形状を表す形状グラフと、データ構造に含まれるオブジェクトの数を表す標識との第２の対応情報を記録する第２の記録部と、第１の記録部により記録された第１の対応情報に含まれる標識と、第２の記録部により記録された第２の対応情報に含まれる標識とに基づいて、データ構造に含まれるオブジェクトの数の増減に関する情報を出力する出力部として機能させる、プログラムも提供する。
【発明の効果】
【００１４】
本発明によれば、任意の種類のデータ構造を対象としてデータ構造の形状の量的な変化を捉えることができる。
【発明を実施するための最良の形態】
【００１５】
以下、添付図面を参照して、本発明を実施するための最良の形態（以下、「実施の形態」という）について詳細に説明する。
まず、本実施の形態の概要について説明する。
本実施の形態では、形状解析に対して、静的形状グラフ（以下、単に「形状グラフ」という）の成分から、その成分が表すオブジェクトの個数を表現する標識の一例である式へのマップを導入する。また、名前付きのノードは、１つのオブジェクトだけを抽象化しているので、そのノードからのマップには1を割り当てる。そして、形状解析を以下のように実行する。
【００１６】
１．解析前の初期状態の形状グラフの意味のある成分に対して、変数m（>= 0）を与える。
２．以下のような条件を考慮して、成分が表すオブジェクトの数のマップを更新する処理を不動点に達するまで繰り返す。
（ア）破壊的代入によって、mにマップされたある成分にm’にマップされた別の成分が連結されたときには、連結後の成分をm+m’へマップする。
（イ）１つのノードが到達可能でなくなったときには、そのノードを含んでいたマップにおけるオブジェクトの数から1を引く。
（ウ）到達可能でなくなったオブジェクトの数が不明のときは、残りの成分をオブジェクト数不明Τにマップする。
（エ）オブジェクト数に変化がない成分は元々の数にマップする。
（オ）制御フローの合流点で同一の成分が違う値で表現されていたら、安全性を保つためにオブジェクト数不明Τに置き換える。
３．不動点到達後に、mの関数として表されたオブジェクト数へのマップが意味のある答えとなる。
【００１７】
形状解析には様々なバリエーションが存在するが、ここでは、非特許文献１で提案されたものに適用する。その概要を図１に示す。この図に示すように、本実施の形態では、破線で囲まれた部分の成分が何個のオブジェクトを表現するものであるかという情報が追加されている。
【００１８】
ここで、本実施の形態の前提となる形状グラフ、オブジェクト数、マップを定義する。但し、簡単化のためにノードの共有に関する情報は省いて述べる。
まず、形状グラフSGは、変数の集合PVar、ノードの集合{nX | X ⊆ PVar}、変数辺Ev、セレクタ辺Esから成り立つ有向グラフとして定義される。ここで、Evは<x, n>（x ∈PVar、nはノード）、Esは<s, sel, t>（s, tはノード、selはcar, cdr等のオブジェクトのセレクタ）である。
【００１９】
図２に、形状グラフの一例を示す。この例は、変数xから指されたリストを示しており、この形状グラフによって表現されるリストは、データ構造の一例である。尚、図中、n{x}は変数xにより指されるノードを意味し、nφは、プログラム中の変数から直接指されないノードを意味する。
【００２０】
また、オブジェクト数Eは、以下のような言語で定義された式で表される。
E ::= E op E | 変数 | 自然数
op = + | - | *
言い換えると、オブジェクト数は、変数又は自然数或いはその両方の足し算、引き算、掛け算からなる式で表現される。
【００２１】
更に、形状グラフの成分c ⊆SGには、オブジェクト数がマップD: 2SG→Eによって割り当てられる。Xがφ（空集合）でないnXだけを含む成分、つまり、変数辺が{<x, nX> | x∈X}で、セレクタ辺がφである成分には、1が割り当てられる。また、オブジェクトの個数が不明の成分はΤへマップされる。
そして、非特許文献１の方法に従って形状解析を行う。
【００２２】
次に、このような形状解析を行うプログラム解析装置の機能構成について説明する。このプログラム解析装置は、例えば、プログラムの開発を支援する装置の一部として実現するとよい。
図３は、プログラム解析装置の機能構成例を示したブロック図である。
図示するように、プログラム解析装置１０は、プログラム記憶部１１と、制御フローグラフ生成部１２と、制御フローグラフ記憶部１３と、初期マップ生成部１４と、マップ記憶部１５とを備える。また、データフロー方程式生成部１６と、データフロー方程式記憶部１７と、マップ更新部１８とを備える。
【００２３】
プログラム記憶部１１は、解析対象のプログラムを記憶する。例えば、磁気ディスクによって構成するとよい。
制御フローグラフ生成部１２は、プログラム記憶部１１に記憶されたプログラムを既存技術を用いて解析し、制御フローグラフを生成する。
制御フローグラフ記憶部１３は、制御フローグラフ生成部１２が生成した制御フローグラフを記憶する。例えば、磁気ディスクによって構成するとよい。
初期マップ生成部１４は、制御フローグラフの各基本ブロックの入口及び出口について、形状グラフとオブジェクト数とのマップを記録する領域を確保し、この領域に初期マップを記録する。本実施の形態では、プログラムの実行前におけるデータ構造の形状を表す形状グラフと、そのデータ構造に含まれるオブジェクトの数を表す標識との第１の対応情報を記録する第１の記録部の一例として、初期マップ生成部１４を設けている。
マップ記憶部１５は、制御フローグラフの各基本ブロックの入口及び出口に対する形状グラフとオブジェクト数とのマップを記憶する。例えば、磁気ディスクによって構成するとよい。
【００２４】
データフロー方程式生成部１６は、制御フローグラフに基づいてデータフロー方程式を生成する。本実施の形態では、ステートメントを取得する取得部の一例として、データフロー方程式生成部１６を設けている。
データフロー方程式記憶部１７は、データフロー方程式生成部１６が生成したデータフロー方程式を記憶する。例えば、磁気ディスクによって構成するとよい。
マップ更新部１８は、データフロー方程式に基づいて、マップ記憶部１５に記憶されたマップを更新する。本実施の形態では、プログラムの実行後におけるデータ構造の形状を表す形状グラフと、そのデータ構造に含まれるオブジェクトの数を表す標識との第２の対応情報を記録する第２の記録部の一例として、マップ更新部１８を設けている。
【００２５】
次に、プログラム解析装置１０の動作について説明する。
図４は、プログラム解析装置１０の動作例を示したフローチャートである。
プログラム解析装置１０では、まず、制御フローグラフ生成部１２が、プログラム記憶部１１に記憶されたプログラムを読み込み、図１に示したような制御フローグラフを生成して制御フローグラフ記憶部１３に記憶する（ステップ１０１）。この制御フローグラフは、既存技術を用いて生成すればよいので、詳細な説明は省略する。このステップ１０１の処理の結果、図１の制御フローグラフにおいて四角形で示した基本ブロックとそれらをつなぐ辺とが生成される。尚、本実施の形態では、説明の簡単化のために１つの文（ステートメント）が１つの基本ブロックに含まれていると仮定する。また、基本ブロックvに先行する基本ブロックの集合をpred(v)と表記することにする。
【００２６】
次に、初期マップ生成部１４が、制御フローグラフ記憶部１３から制御フローグラフに含まれる基本ブロックの情報を読み出し、各基本ブロックの入口INと出口OUTに対して、初期マップを与える（ステップ１０２）。例えば、制御フローグラフに含まれる基本ブロックごとの領域をマップ記憶部１５に設け、各領域を入口におけるマップ用の領域と出口におけるマップ用の領域とに更に分け、該当する領域に初期マップを記憶する。
【００２７】
ここでは、対象のプログラムに入力されるオブジェクトはその個数が未知であるので、入力全体を表すグラフSG0に変数m（>=0）を割り当てる（DにSG0→mを加える）。或いは、n個の入力を取るプログラムの入力xi（0<=i<n）がノードを共有しないことを前提に、xiから到達可能な辺とノードからなる成分ci⊆SG0に対してmi（>=0）を割り当てる（Dにci→miを加える）。前者は、プログラムの実行によって全体のオブジェクト数がどのように増減するかを知るために用いられ、後者は、入力ごとの変化を知るために用いられる。本実施の形態では、オブジェクトの型が１つしかない場合を仮定してグラフ全体に変数を割り当てているが、形状グラフでオブジェクトの型を区別して表現する場合には、型ごとに成分を作り別の変数を割り当ててもよい。この場合は、型別にオブジェクトの個数の変化を知ることができる。
【００２８】
次いで、データフロー方程式生成部１６は、制御フローグラフ記憶部１３に記憶された制御フローグラフに基づいてデータフロー方程式を作成し、データフロー方程式記憶部１７に記憶する（ステップ１０３）。ここでは、後述する伝達関数以外は既存技術を用いる。制御フローグラフの各基本ブロックvi（iは基本ブロックのＩＤ）に関して、以下のような方程式を立てる。
【００２９】
【数１】
2010020558.tif 000003
【００３０】
この方程式は、ある基本ブロックviの入力はそれに先行するブロックの出力を併合したものであることを表す。この併合演算は後述する。また、先行する基本ブロックが１つしかないときには、そのままその基本ブロックの出力が渡される。
【００３１】
【数２】
2010020558.tif 000004
【００３２】
この方程式のF[st]は、基本ブロックviで実行する文をstとしたときの伝達関数であり、以下のように定義される。即ち、オブジェクト数を考慮しない形状解析における、文stを実行するときの伝達関数をf[st]: SG→SGとする。すると、F[st]は、入力のマップDの各要素c→eを、その基本ブロックが実行する文stに応じてマップDに追加する要素に変換する関数である。
以下、F[st]による要素の変換方法について詳細に述べる。尚、ここでは、ノードが変数から到達できなくなることを「ゴミになる」と表現する。
【００３３】
1  stが「x := nil」のタイプの式の場合：
1.1  cにn{x}が存在して、<*, *, n{x}>が存在しなかった場合（*は任意のノード、セレクタを表す）：
1.1.1  <n{x}, *, nφ>及び<nφ, *, nφ>が存在した場合：オブジェクトが何個ゴミになるか不明なので、f(c)→ΤをDに加える。
1.1.2  その他の場合：SGからSG’への変換と同様にfによってcを変換し、Dにf(c)→e-1を加える。これは、n{x}だけがゴミになるような場合である。
1.2  その他の場合：f(c)→eをDに加える。個数がeのまま変化しないのは、マップされる成分中のオブジェクトの数が変化しないからである。
【００３４】
2  stが「x.sel := nil」のタイプの式の場合：
2.1  cに<nX, sel, nφ>, x∈Xという辺が存在する場合：
2.1.1  nφが非共有の場合：
2.1.1.1  <nφ, sel’, nφ>が存在する場合：
2.1.1.1.1  <nY, sel’’, nφ>, X∩Y＝φ∨sel’’≠selが存在する場合：何個ゴミになるか不明なので、f(c)→ΤをDに加える。
2.1.1.1.2  その他の場合：何個ゴミになるか不明だが、生き残るオブジェクト数は分かる。そしてf(c)はnφを含まないはずなので、自明なマップf(c)→(f(c)の名前付きノードの数)をDに加える。
2.1.1.2  その他の場合：1.1.2と同様にf(c)→e-1をDに加える。これは、nφで要約されていたオブジェクトが１つゴミになるような場合である。
2.1.2  nφが共有の場合：f(c)の個数は不明なので、f(c)→ΤをDに加える。
2.2  その他の場合：1.2と同様。ここで、f(c)は非連結な要素で構成されてしまうが、特に問題ない。
【００３５】
3  stが「x.sel := y」のタイプの式の場合：
3.1  cにyが含まれていた場合：1.2と同様、既にマップされている要素の中で辺を付け足しただけであり、オブジェクト数は変化しないので、f(c)→eをDに加える。
3.2  cにyが含まれていなかった場合：c’がyを含み、かつ、c’に含まれる全ての変数辺がcの変数辺とコンパチブルであり、Dがc’→e’を含むとすると、f(c∪c’)→e+e’をDに加える。ここで、形状グラフのある成分（上記ではc'）における変数辺<y, nY>(y∈Y)が別の成分（上記ではc）における変数辺<x, nX>(x∈X)と「コンパチブル」であるとは、X∩Y=φ（XとYの共通部分が空集合）であることをいう。また、c∪c’は、(cの変数辺)∪(c’の変数辺)と(cのセレクタ辺)∪(c’のセレクタ辺)で構成される成分の意味である。
4  その他の場合：1.2と同様に、f(c)→eをDに加える。
【００３６】
ところで、f(c)→e1，f(c)→e2，e1≠e2のようにD内でマップがぶつかってしまうことがある。このときは、後述の関数joinを使って、f(c)→e1及びf(c)→e2をf(c)→join(e1，e2)に置き換える。
先に述べた入力に関するデータフロー方程式では、制御の合流点Vにおいて演算∪により入力を併合した。この併合演算∪は、関数joinを用いて、以下のように定義される。
即ち、D1とD2が入力としてデータフロー方程式から与えられた場合に、出力D’は、
{d1 | d1∈D1，d1=c1→e1，∀d2∈D2，d2=c2→e2，c1≠c2} ∪
{d2 | d2∈D2，d2=c2→e2，∀d1∈D1，d1=c1→e1，c1≠c2} ∪
{d3 | d3=c12→join(e1，e2)，d1∈D1，d1=c12→e1，∃d2∈D2，d2=c12→e2，e1≠e2} ∪
{d12 | d12∈D1，d12∈D2}
となる。
【００３７】
ここで、関数join: E×E→Eは、次のように定義される。
1.  e1, e2の差が定数kのとき：join(e1, e2) = e1＋k*iとする。iは新たに導入された変数で、Vが帰り辺との合流点の場合は、i>=0である。尚、このときのiはループの実行回数と関連する。また、Vがその他の合流点の場合やDで衝突が起きた場合は、i∈{0, 1}とする。尚、このときのiはif文などの条件と関連する。これらの新しく導入された変数iは、他の静的解析の結果を用いたり、それへの入力に用いたりすることができる。
2.  e1, e2が上記以外場合：join(e1, e2) =Τとする。
【００３８】
尚、入力が３つ以上の場合は、この演算を繰り返すことにより、２つの入力に対する演算の組み合わせとして実行すればよい。この演算は結合法則が成り立つので、どのように組み合わせてもよい。最も簡単なのは、例えば∪(D1, D2, D3) のような３入力の場合に、∪(∪(D1, D2), D3)と左側から結合してしまうことである。
【００３９】
次に、マップ更新部１８は、この伝達関数F[st]と合流点における演算∪とを用いて、成分に割り当てられたオブジェクト数を更新していく（ステップ１０４）。つまり、マップ記憶部１５に記憶されたマップを更新していく。
その後、マップ更新部１８は、マップに変化があったかどうかを判定する（ステップ１０５）。そして、変化があれば、ステップ１０４の処理を繰り返す。また、変化がなければ、処理を終了する。即ち、最終的にはマップが不動点に達し、その時点でマップ記憶部１５に記憶されている内容が、例えば、出力部の一例である表示機構９０ｄ（図１３参照）に出力される。これにより、プログラムの各ポイントにおけるオブジェクトの個数の変化を知ることができる。
【００４０】
次に、図４のフローチャートに沿った動作を行うことにより更新されるマップ記憶部１５の内容について説明する。
図５は、マップ記憶部１５の内容の一例を示したものである。ここでは、ステップ１０２で初期マップが生成された時点でのマップ記憶部１５の内容を示している。IN1以外は、この段階では全く分からないので、何も記録されていない。その後、ステップ１０４で基本ブロックv1に含まれる文stを処理すると、OUT1が記録される。また、基本ブロックv2,v3,v4,…に含まれる文stを処理すると、IN2,OUT2,IN3,OUT3,IN4,OUT4,…が順次記録されていく。
【００４１】
次いで、図４のフローチャートにおけるステップ１０４の処理を詳細に説明する。尚、ステップ１０４では、全ての基本ブロックに対するマップを更新してもよいし、マップに変化を及ぼす基本ブロックのみを既存技術により選択してその基本ブロックに対するマップを更新してもよい。即ち、通常、複数の基本ブロックに対するマップを更新するが、ここでは、説明を簡単化するため、１つの基本ブロックに対するマップの更新のみに着目して説明するものとする。また、１つの基本ブロックに対するマップの更新は、更に、出力に関するデータフロー方程式に基づくマップの更新と、入力に関するデータフロー方程式に基づくマップの更新とを含むので、これらを分けて説明する。
【００４２】
まず、ある基本ブロックの出力に関するデータフロー方程式に基づくマップ（OUT）を登録するOUT登録処理の動作を説明する。
図６は、このときのマップ更新部１８の動作を示したフローチャートである。尚、この動作の前提として、この基本ブロックに入力されるマップの要素c→eも図示しないメモリに保持しておくものとする。その際、入力されるマップの要素としては、連続する基本ブロックを処理する場合であれば、１つ前の基本ブロックを処理する際にメモリに記憶されていたものをそのまま用いてもよいし、マップ記憶部１５から読み出したものを用いてもよい。
まず、マップ更新部１８は、データフロー方程式記憶部１７に記憶されたこの基本ブロックに対応するデータフロー方程式から、文stを取得する（ステップ２０１）。
【００４３】
次に、マップ更新部１８は、ステップ２０１で取得した文stが「x := nil」のタイプの式であるかどうかを判定する（ステップ２０２）。そして、「x := nil」のタイプの式であれば、後述するOUT登録処理１を実行し（ステップ２０３）、「x := nil」のタイプの式でなければ、次の処理に進む。
また、マップ更新部１８は、ステップ２０１で取得した文stが「x.sel := nil」のタイプの式であるかどうかを判定する（ステップ２０４）。そして、「x.sel := nil」のタイプの式であれば、後述するOUT登録処理２を実行し（ステップ２０５）、「x.sel := nil」のタイプの式でなければ、次の処理に進む。
更に、マップ更新部１８は、ステップ２０１で取得した文stが「x.sel := y」のタイプの式であるかどうかを判定する（ステップ２０６）。そして、「x.sel := y」のタイプの式であれば、後述するOUT登録処理３を実行し（ステップ２０７）、「x.sel := y」のタイプの式でなければ、f(c)→eをマップ記憶部１５に記憶する（ステップ２０８）。
【００４４】
ここで、文stが「x := nil」のタイプの式である場合に実行されるOUT登録処理１の動作を説明する。
図７は、このときのマップ更新部１８の動作を示したフローチャートである。
まず、マップ更新部１８は、図示しないメモリ内に保持されたcが、n{x}を含み、かつ、<*, *, n{x}>を含まないかどうかを判定する（ステップ２２１）。
その結果、cが、n{x}を含み、かつ、<*, *, n{x}>を含まないと判定した場合、マップ更新部１８は、cが<n{x}, *, nφ>及び<nφ, *, nφ>を含むかどうかを判定する（ステップ２２２）。そして、cが<n{x}, *, nφ>及び<nφ, *, nφ>を含めば、f(c)→Τをマップ記憶部１５に記憶する（ステップ２２３）。また、cが<n{x}, *, nφ>及び<nφ, *, nφ>を含まなければ、f(c)→e-1をマップ記憶部１５に記憶する（ステップ２２４）。
一方、ステップ２２１で、cが、n{x}を含み、かつ、<*, *, n{x}>を含まない、という条件が成立しないと判定した場合、マップ更新部１８は、f(c)→eをマップ記憶部１５に記憶する（ステップ２２５）。
【００４５】
また、文stが「x.sel := nil」のタイプの式である場合に実行されるOUT登録処理２の動作を説明する。
図８は、このときのマップ更新部１８の動作を示したフローチャートである。
まず、マップ更新部１８は、図示しないメモリ内に保持されたcが、<nX, sel, nφ>（x∈X）という辺を含むかどうかを判定する（ステップ２４１）。
その結果、cが、<nX, sel, nφ>（x∈X）という辺を含むと判定した場合、マップ更新部１８は、nφが共有かどうかを判定する（ステップ２４２）。そして、nφが共有でないと判定すると、cが<nφ, sel’, nφ>を含むかどうかを判定する（ステップ２４３）。その結果、cが<nφ, sel’, nφ>を含むと判定すれば、マップ更新部１８は、cが<nY, sel’’, nφ>（X∩Y＝φ∨sel’’≠sel）を含むかどうかを判定する（ステップ２４４）。そして、cが<nY, sel’’, nφ>（X∩Y＝φ∨sel’’≠sel）を含めば、f(c)→Τをマップ記憶部１５に記憶する（ステップ２４５）。また、cが<nY, sel’’, nφ>（X∩Y＝φ∨sel’’≠sel）を含まなければ、f(c)→(f(c)の名前付きノードの数)をマップ記憶部１５に記憶する（ステップ２４６）。
一方、ステップ２４３で、cが<nφ, sel’, nφ>を含まないと判定した場合、マップ更新部１８は、f(c)→e-1をマップ記憶部１５に記憶する（ステップ２４７）。
また、ステップ２４２で、nφが共有であると判定した場合、マップ更新部１８は、f(c)→Τをマップ記憶部１５に記憶する（ステップ２４５）。
更に、ステップ２４１で、cが、<nX, sel, nφ>（x∈X）という辺を含まないと判定した場合、マップ更新部１８は、f(c)→eをマップ記憶部１５に記憶する（ステップ２４８）。
【００４６】
更に、文stが「x.sel := y」のタイプの式である場合に実行されるOUT登録処理３の動作を説明する。
図９は、このときのマップ更新部１８の動作を示したフローチャートである。
まず、マップ更新部１８は、図示しないメモリ内に保持されたcがyを含むかどうかを判定する（ステップ２６１）。
その結果、cがyを含むと判定した場合、マップ更新部１８は、f(c)→Τをマップ記憶部１５に記憶する（ステップ２６２）。一方、cがyを含まないと判定した場合、マップ更新部１８は、上記3.2に記した条件を満たすc’があることを前提として、f(c∪c’)→e+e’をマップ記憶部１５に記憶する（ステップ２６３）。
【００４７】
次に、ある基本ブロックの入力に関するデータフロー方程式に基づくマップ（IN）を登録するIN登録処理の動作を説明する。
図１０は、このときのマップ更新部１８の動作を示したフローチャートである。尚、この動作の前提として、この基本ブロックに先行する基本ブロックから出力されたマップの要素f(c)→eも図示しないメモリに保持しておくものとする。その際、出力されたマップの要素としては、連続する基本ブロックを処理する場合であれば、１つ前の基本ブロックを処理する際にメモリに記憶されていたものをそのまま用いてもよいし、マップ記憶部１５から読み出したものを用いてもよい。
まず、マップ更新部１８は、この基本ブロックに入力されるマップの要素に、同一の成分に対して異なる値が割り当てられたものがあるか、つまり、f(c)→e1及びf(c)→e2（e1≠e2）があるかどうかを判定する（ステップ３０１）。
その結果、f(c)→e1及びf(c)→e2（e1≠e2）があると判定した場合、マップ更新部１８は、e1とe2の差が定数kであるかどうかを判定する（ステップ３０２）。そして、e1とe2の差が定数kであれば、join(e1, e2) = e1＋k*iとし、f(c)→e1及びf(c)→e2をf(c)→join(e1，e2)に置き換える（ステップ３０３）。また、e1とe2の差が定数kでなければ、join(e1, e2) = Tとし、f(c)→e1及びf(c)→e2をf(c)→join(e1，e2)に置き換える（ステップ３０４）。
一方、f(c)→e1及びf(c)→e2（e1≠e2）がないと判定した場合は、そのまま次の処理に進む。
その後、マップ更新部１８は、上記併合演算∪を用いて計算された要素をマップ記憶部１５に記憶する（ステップ３０５）。
【００４８】
このように、本実施の形態では、形状グラフの成分とオブジェクト数との対応を更新することにより、プログラムの各ポイントにおけるオブジェクト数の変化を分かるようにした。そして、開発補助ツールは、この情報をプログラマに提示することにより、プログラム理解を助けることができる。また、静的解析ツール等の応用プログラムは、この情報を用いてプログラムが正しく動作するかを検証することができる。
【００４９】
以下、本実施の形態を実際のプログラムに適用した実行例を記す。
［実行例］Ｔｒｅｅへの要素の追加
この実行例では、セレクタとしてcar，cdrの２つのセレクタを用いた木のある場所に要素を追加するプログラムinsertとその実行履歴を示す。v1とv18において、形状グラフは同一だが、要素が１つ増えていることが分かる。
図１１に、正規化された解析対象のプログラムを示す。
また、図１２に、正規化したコードの制御フローグラフを示す。
【００５０】
ステップ１０４で対象とする基本ブロック及びその処理順序については、種々の方法があるが、ここでは、初めにループ以前の基本ブロック（v1〜v2）を１回、次にループ内の基本ブロック（v3〜v8）を３回、最後にループ以後の基本ブロック（v9〜v17）を１回処理する場合について説明する。他の処理順序でも同様の解が導けるが、この方法が最短で解が導ける手順である。
そして、以下では、各基本ブロックについて、入力となるマップであるマップ（IN）（必要な場合のみ）と、出力となるマップであるマップ（OUT）とを記述する。また、計算に関係のあるデータフロー方程式もこれらの間に示す。
尚、以下の記述中、「条件」とは、先にF[st]の定義で場合分けを行った際の各場合分けに付した項番に対応する。また、これまでは、個数の可能性が無限にあるオブジェクトを抽象化したノードをnφで表したが、この実行例ではn{}で表す。更に、マップ中の変数辺はセレクタ辺から自明なので、省略する。
【００５１】
＜ループ以前の基本ブロックの処理経過＞
・マップ（IN）:
IN1: ステップ１０２における初期化処理の後の状態。以下では自明なマップ[<e, n{e}>]->1は省略する。
Ev: <x, n{x}>, <e, n{e}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００５２】
・データフロー方程式：
OUT1 = F[y:= nil](IN1)
・マップ（OUT）:
OUT1: 条件1.2に該当し、変化無し。
Ev: <x, n{x}>, <e, n{e}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００５３】
・データフロー方程式：
IN2 = OUT1
OUT2 = F[y := x](IN2)
・マップ（OUT）:
OUT2: stがy:=xで、条件4に該当する。n{x}がn{x,y}に変わった。
Ev: <x, n{x,y}>, <y, n{x,y}>, <e, n{e}>
Es: <n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００５４】
＜１回目のループ内の基本ブロックの処理経過＞
・データフロー方程式：
IN3 = ∪(OUT2, OUT8) = OUT2 (∵OUT8 = φ)
OUT3 = F[whileの中の条件](IN3)
・マップ（OUT）:
OUT3: 条件4に該当し、変化無し。
Ev: <x, n{x,y}>, <y, n{x,y}>, <e, n{e}>
Es: <n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００５５】
・データフロー方程式：
IN4 = OUT3
OUT4 = F[z := nil](IN4)
・マップ（OUT）:
OUT4: 条件1.2に該当し、変化無し。
Ev: <x, n{x,y}>, <y, n{x,y}>, <e, n{e}>
Es: <n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００５６】
（基本ブロックv5はif文のthen節の方）
・データフロー方程式：
IN5 = OUT4
OUT5 = F[z := y.car](IN5)
・マップ（OUT）:
OUT5：条件4に該当する。マップの元は変化するが、個数には変化無し。
Ev: <x, n{x,y}>, <y, n{x,y}>, <z, n{z}>, <e, n{e}>
Es: <n{x,y}, car, n{z}>, <n{x,y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x,y}, car, n{z}>, <n{x,y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００５７】
（基本ブロックv6はif文のelse節の方）
・データフロー方程式：
IN6 = OUT4
OUT6 = F[z := y.cdr](IN6)
・マップ（OUT）:
OUT6：条件4に該当する。マップの元は変化するが、個数には変化無し。
Ev: <x, n{x,y}>, <y, n{x,y}>, <z, n{z}>, <e, n{e}>
Es: <n{x,y}, car, n{}>, <n{x,y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x,y}, car, n{}>, <n{x,y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００５８】
・データフロー方程式：
IN7 = ∪(OUT5, OUT6)
・マップ（IN）:
IN7：v5からの辺とv6からの辺が合流するので、それらの和集合をとる。
Ev: <x, n{x,y}>, <y, n{x,y}>, <z, n{z}>, <e, n{e}>
Es: <n{x,y}, car, n{z}>, <n{x,y}, cdr, n{z}>, <n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x,y}, car, n{z}>, <n{x,y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x,y}, car, n{}>, <n{x,y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００５９】
・データフロー方程式：
OUT7 = F[y := nil](IN7)
・マップ（OUT）:
OUT7：条件1.2に該当する。
Ev: <x, n{x}>, <z, n{z}>, <e, n{e}>
Es: <n{x}, car, n{z}>, <n{x}, cdr, n{z}>, <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{z}>, <n{x}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００６０】
・データフロー方程式：
IN8 = OUT7
OUT8 = F[y := z](IN8)
・マップ（OUT）:
OUT8：条件4に該当する。
Ev: <x, n{x}>, <y, n{y,z}>, <z, n{y,z}>, <e, n{e}>
Es: <n{x}, car, n{y,z}>, <n{x}, cdr, n{y,z}>, <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{y,z}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００６１】
＜２回目のループ内の基本ブロックの処理経過＞
・データフロー方程式：
IN3 = ∪(OUT2, OUT8)
・マップ（IN）:
IN3：OUT2とOUT8の和集合。
Ev: <x, n{x}>, <y, n{y,z}>, <z, n{y,z}>, <x, n{x,y}>, <y, n{x,y}>, <e, n{e}>
Es: <n{x}, car, n{y,z}>, <n{x}, cdr, n{y,z}>, <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{y,z}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００６２】
・データフロー方程式：
OUT3 = F[whileの中の条件](IN3)
・マップ（OUT）:
OUT3：条件4に該当し、変化無し。
Ev: <x, n{x}>, <y, n{y,z}>, <z, n{y,z}>, <x, n{x,y}>, <y, n{x,y}>, <e, n{e}>
Es: <n{x}, car, n{y,z}>, <n{x}, cdr, n{y,z}>, <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{y,z}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００６３】
・データフロー方程式：
IN4 = OUT3
OUT4 = F[z := nil](IN4)
・マップ（OUT）:
OUT4：条件1.2に該当する。
Ev: <x, n{x}>, <y, n{y}>, <x, n{x,y}>, <y, n{x,y}>, <e, n{e}>
Es: <n{x}, car, n{y}>, <n{x}, cdr, n{y}>, <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{y}, car, n{}>, <n{y}, cdr, n{}>, <n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{y}>, <n{x}, cdr, n{}>, <n{y}, car, n{}>, <n{y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{y}>, <n{y}, car, n{}>, <n{y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００６４】
・データフロー方程式：
IN5 = OUT4
OUT5 = F[z := y.car](IN5)
・マップ（OUT）:
OUT5： 条件4に該当する。
Ev: <x, n{x}>, <y, n{y}>, <x, n{x,y}>, <y, n{x,y}>, <z, n{z}>, <e, n{e}>
Es: <n{x}, car, n{y}>, <n{x}, cdr, n{y}>, <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{y}, car, n{z}>, <n{y}, cdr, n{}>, <n{x,y}, car, n{z}>, <n{x,y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{y}>, <n{x}, cdr, n{}>, <n{y}, car, n{z}>, <n{y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{y}>, <n{y}, car, n{z}>, <n{y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x,y}, car, n{z}>, <n{x,y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００６５】
・データフロー方程式：
IN6 = OUT4
OUT6 = F[z :=y.cdr](IN6)
・マップ（OUT）:
OUT6：条件4に該当する。
Ev: <x, n{x}>, <y, n{y}>, <x, n{x,y}>, <y, n{x,y}>, <z, n{z}>, <e, n{e}>
Es: <n{x}, car, n{y}>, <n{x}, cdr, n{y}>, <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{y}, car, n{}>, <n{y}, cdr, n{z}>, <n{x,y}, car, n{}>, <n{x,y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{y}>, <n{x}, cdr, n{}>, <n{y}, car, n{}>, <n{y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{y}>, <n{y}, car, n{}>, <n{y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x,y}, car, n{}>, <n{x,y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００６６】
・データフロー方程式：
IN7 = ∪(OUT5, OUT6)
・マップ（IN）:
IN7：v5からの辺とv6からの辺が合流するので、それらの和集合をとる。
Ev: <x, n{x}>, <y, n{y}>, <x, n{x,y}>, <y, n{x,y}>, <z, n{z}>, <e, n{e}>
Es: <n{x}, car, n{y}>, <n{x}, cdr, n{y}>, <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{y}, car, n{z}>, <n{y}, cdr, n{z}>, <n{y}, car, n{}>, <n{y}, cdr, n{}>, <n{x,y}, car, n{z}>, <n{x,y}, cdr, n{z}>, <n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{y}>, <n{x}, cdr, n{}>, <n{y}, car, n{z}>, <n{y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{y}>, <n{x}, cdr, n{}>, <n{y}, car, n{}>, <n{y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{y}>, <n{y}, car, n{z}>, <n{y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{y}>, <n{y}, car, n{}>, <n{y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x,y}, car, n{z}>, <n{x,y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x,y}, car, n{}>, <n{x,y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００６７】
・データフロー方程式：
OUT7 = F[y := nil](IN7)
・マップ（OUT）:
OUT7：条件1.2に該当する。
Ev: <x, n{x}>, <z, n{z}>, <e, n{e}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{z}>, <n{}, cdr, n{z}>, <n{x}, car, n{z}>, <n{x}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{z}>, <n{x}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００６８】
・データフロー方程式：
IN8 = OUT7
OUT8 = F[y := z](IN8)
・マップ（OUT）:
OUT8：条件4に該当する。
Ev: <x, n{x}>, <y, n{y,z}>, <z, n{y,z}>, <e, n{e}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y,z}>, <n{}, cdr, n{y,z}>, <n{x}, car, n{y,z}>, <n{x}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{y,z}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００６９】
＜３回目のループ内の基本ブロックの処理経過＞
・データフロー方程式：
IN3 = ∪(OUT2, OUT8)
IN3：OUT2とOUT8の和集合。
Ev: <x, n{x}>, <y, n{y,z}>, <z, n{y,z}>, <x, n{x,y}>, <y, n{x,y}>, <e, n{e}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y,z}>, <n{}, cdr, n{y,z}>, <n{x}, car, n{y,z}>, <n{x}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{y,z}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００７０】
・データフロー方程式：
OUT3 = F[while文の条件](IN3)
・マップ（OUT）:
OUT3： 条件4に該当し、変化無し。
Ev: <x, n{x}>, <y, n{y,z}>, <z, n{y,z}>, <x, n{x,y}>, <y, n{x,y}>, <e, n{e}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y,z}>, <n{}, cdr, n{y,z}>, <n{x}, car, n{y,z}>, <n{x}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{y,z}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００７１】
・データフロー方程式：
IN4 = OUT3
OUT4 = F[z := nil](IN4)
・マップ（OUT）:
OUT4：条件1.2に該当する。
Ev: <x, n{x}>, <y, n{y}>, <x, n{x,y}>, <y, n{x,y}>, <e, n{e}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y}>, <n{}, cdr, n{y}>, <n{x}, car, n{y}>, <n{x}, cdr, n{y}>, <n{y}, car, n{}>, <n{y}, cdr, n{}>, <n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y}>, <n{y}, car, n{}>, <n{y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, cdr, n{y}>, <n{y}, car, n{}>, <n{y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{y}>, <n{x}, cdr, n{}>, <n{y}, car, n{}>, <n{y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{y}>, <n{y}, car, n{}>, <n{y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００７２】
・データフロー方程式：
IN5 = OUT4
OUT5 = F[z := y.car](IN5)
・マップ（OUT）:
OUT5：条件4に該当する。
Ev: <x, n{x}>, <y, n{y}>, <x, n{x,y}>, <y, n{x,y}>, <z, n{z}>, <e, n{e}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y}>, <n{}, cdr, n{y}>, <n{z}, car, n{y}>, <n{z}, cdr, n{y}>, <n{x}, car, n{y}>, <n{x}, cdr, n{y}>, <n{y}, car, n{z}>, <n{y}, cdr, n{}>, <n{x,y}, car, n{z}>, <n{x,y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y}>, <n{z}, car, n{y}>, <n{y}, car, n{z}>, <n{y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, cdr, n{y}>, <n{z}, cdr, n{y}>, <n{y}, car, n{z}>, <n{y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{y}>, <n{x}, cdr, n{}>, <n{y}, car, n{z}>, <n{y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{y}>, <n{y}, car, n{z}>, <n{y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x,y}, car, n{z}>, <n{x,y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００７３】
・データフロー方程式：
IN6 = OUT4
OUT6 = F[z := y.cdr](IN6)
・マップ（OUT）:
OUT6：条件4に該当する。
Ev: <x, n{x}>, <y, n{y}>, <x, n{x,y}>, <y, n{x,y}>, <z, n{z}>, <e, n{e}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y}>, <n{}, cdr, n{y}>, <n{z}, car, n{y}>, <n{z}, cdr, n{y}>, <n{x}, car, n{y}>, <n{x}, cdr, n{y}>, <n{y}, car, n{}>, <n{y}, cdr, n{z}>, <n{x,y}, car, n{}>, <n{x,y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y}>, <n{z}, car, n{y}>, <n{y}, car, n{}>, <n{y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, cdr, n{y}>, <n{z}, cdr, n{y}>, <n{y}, car, n{}>, <n{y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{y}>, <n{x}, cdr, n{}>, <n{y}, car, n{}>, <n{y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{y}>, <n{y}, car, n{}>, <n{y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x,y}, car, n{}>, <n{x,y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００７４】
・データフロー方程式：
IN7 = ∪(OUT5, OUT6)
・マップ（IN）:
IN7：v5からの辺とv6からの辺が合流するので、それらの和集合をとる。
Ev: <x, n{x}>, <y, n{y}>, <x, n{x,y}>, <y, n{x,y}>, <z, n{z}>, <e, n{e}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y}>, <n{}, cdr, n{y}>, <n{z}, car, n{y}>, <n{z}, cdr, n{y}>, <n{x}, car, n{y}>, <n{x}, cdr, n{y}>, <n{y}, car, n{z}>, <n{y}, cdr, n{z}>, <n{y}, car, n{}>, <n{y}, cdr, n{}>, <n{x,y}, car, n{z}>, <n{x,y}, cdr, n{z}>, <n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y}>, <n{z}, car, n{y}>, <n{y}, car, n{z}>, <n{y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y}>, <n{z}, car, n{y}>, <n{y}, car, n{}>, <n{y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, cdr, n{y}>, <n{z}, cdr, n{y}>, <n{y}, car, n{z}>, <n{y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, cdr, n{y}>, <n{z}, cdr, n{y}>, <n{y}, car, n{}>, <n{y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{y}>, <n{x}, cdr, n{}>, <n{y}, car, n{z}>, <n{y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{y}>, <n{x}, cdr, n{}>, <n{y}, car, n{}>, <n{y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{y}>, <n{y}, car, n{z}>, <n{y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{y}>, <n{y}, car, n{}>, <n{y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x,y}, car, n{z}>, <n{x,y}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x,y}, car, n{}>, <n{x,y}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００７５】
・データフロー方程式：
OUT7 = F[y := nil](IN7)
・マップ（OUT）:
OUT7：条件1.2に該当する。
Ev: <x, n{x}>, <z, n{z}>, <e, n{e}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{z}>, <n{}, cdr, n{z}>, <n{x}, car, n{z}>, <n{x}, cdr, n{z}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{z}>, <n{x}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００７６】
・データフロー方程式：
IN8 = OUT7
OUT8 = F[y := z](IN8)
・マップ（OUT）:
OUT8：条件4に該当する。
Ev: <x, n{x}>, <y, n{y,z}>, <z, n{y,z}>, <e, n{e}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{y,z}>, <n{}, cdr, n{y,z}>, <n{x}, car, n{y,z}>, <n{x}, cdr, n{y,z}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{y,z}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００７７】
＜ループ以後の基本ブロックの処理経過＞
・データフロー方程式：
IN9 = OUT3
IN9: 直前のOUT3と同一のもの。
Ev: <x, n{x}>, <y, n{y,z}>, <z, n{y,z}>, <x, n{x,y}>, <y, n{x,y}>, <e, n{e}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{y,z}>, <n{}, cdr, n{y,z}>, <n{x}, car, n{y,z}>, <n{x}, cdr, n{y,z}>, <n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{y,z}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００７８】
・データフロー方程式：
OUT9 = F[t := y.cdr](IN9)
・マップ（OUT）:
OUT9： 条件4に該当する。
Ev: <x, n{x}>, <y, n{y,z}>, <z, n{y,z}>, <x, n{x,y}>, <y, n{x,y}>, <t, n{t}>, <e, n{e}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{t}>, <n{}, car, n{y,z}>, <n{}, cdr, n{y,z}>, <n{t}, car, n{y,z}>, <n{t}, cdr, n{y,z}>, <n{x}, car, n{y,z}>, <n{x}, cdr, n{y,z}>, <n{x,y}, car, n{}>, <n{x,y}, cdr, n{t}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y,z}>, <n{t}, car, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{t}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, cdr, n{y,z}>, <n{t}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{t}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{y,z}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{t}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{t}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x,y}, car, n{}>, <n{x,y}, cdr, n{t}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００７９】
・データフロー方程式：
IN10 = OUT9
OUT10 = F[e.cdr := nil](IN10)
・マップ（OUT）:
OUT10： 条件2.2に該当する。
Ev: <x, n{x}>, <y, n{y,z}>, <z, n{y,z}>, <x, n{x,y}>, <y, n{x,y}>, <t, n{t}>, <e, n{e}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{t}>, <n{}, car, n{y,z}>, <n{}, cdr, n{y,z}>, <n{t}, car, n{y,z}>, <n{t}, cdr, n{y,z}>, <n{x}, car, n{y,z}>, <n{x}, cdr, n{y,z}>, <n{x,y}, car, n{}>, <n{x,y}, cdr, n{t}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y,z}>, <n{t}, car, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{t}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, cdr, n{y,z}>, <n{t}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{t}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{y,z}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{t}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x}, car, n{}>, <n{x}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{t}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
[<n{x,y}, car, n{}>, <n{x,y}, cdr, n{t}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m
【００８０】
・データフロー方程式：
IN11 = OUT10
OUT11 = F[e.cdr := t](IN11)
・マップ（OUT）:
OUT11：条件3.2に該当する。n{e}が1という自明なマップを使用する。
Ev: <x, n{x}>, <y, n{y,z}>, <z, n{y,z}>, <x, n{x,y}>, <y, n{x,y}>, <t, n{t}>, <e, n{e}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{t}>, <n{}, car, n{y,z}>, <n{}, cdr, n{y,z}>, <n{t}, car, n{y,z}>, <n{t}, cdr, n{y,z}>, <n{x}, car, n{y,z}>, <n{x}, cdr, n{y,z}>, <n{x,y}, car, n{}>, <n{x,y}, cdr, n{t}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{e}, cdr, n{t}>, <n{}, car, n{}>, <n{}, cdr, n{}>
is#(n{t}): true
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y,z}>, <n{t}, car, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{t}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{e}, cdr, n{t}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, cdr, n{y,z}>, <n{t}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{t}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{e}, cdr, n{t}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x}, car, n{y,z}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{t}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{e}, cdr, n{t}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x}, car, n{}>, <n{x}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{t}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{e}, cdr, n{t}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x,y}, car, n{}>, <n{x,y}, cdr, n{t}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{e}, cdr, n{t}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
【００８１】
・データフロー方程式：
IN12 = OUT11
OUT12 = F[y.cdr := nil](IN12)
・マップ（OUT）:
OUT12：条件2.2に該当する。
Ev: <x, n{x}>, <y, n{y,z}>, <z, n{y,z}>, <x, n{x,y}>, <y, n{x,y}>, <t, n{t}>, <e, n{e}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{}, car, n{y,z}>, <n{}, cdr, n{y,z}>, <n{t}, car, n{y,z}>, <n{t}, cdr, n{y,z}>, <n{x}, car, n{y,z}>, <n{x}, cdr, n{y,z}>, <n{x,y}, car, n{}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{e}, cdr, n{t}>, <n{}, car, n{}>, <n{}, cdr, n{}>
is#(n{t}): false
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y,z}>, <n{t}, car, n{y,z}>, <n{y,z}, car, n{}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{e}, cdr, n{t}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, cdr, n{y,z}>, <n{t}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{e}, cdr, n{t}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x}, car, n{y,z}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{e}, cdr, n{t}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x}, car, n{}>, <n{x}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{e}, cdr, n{t}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x,y}, car, n{}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{e}, cdr, n{t}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
【００８２】
・データフロー方程式：
IN13 = OUT12
OUT13 = F[y.cdr := e](IN13)
・マップ（OUT）:
OUT13：条件3.1に該当する。
Ev: <x, n{x}>, <y, n{y,z}>, <z, n{y,z}>, <x, n{x,y}>, <y, n{x,y}>, <t, n{t}>, <e, n{e}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{e}>, <n{}, car, n{y,z}>, <n{}, cdr, n{y,z}>, <n{t}, car, n{y,z}>, <n{t}, cdr, n{y,z}>, <n{x}, car, n{y,z}>, <n{x}, cdr, n{y,z}>, <n{x,y}, car, n{}>, <n{x,y}, cdr, n{e}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{e}, cdr, n{t}>, <n{}, car, n{}>, <n{}, cdr, n{}>
is#(n{e}): false /* n{e}はn{x,y}とn{y,z}から指されているが，それらはコンパチブルでないのでis#(n{e})はtrueにならない*/
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y,z}>, <n{t}, car, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{e}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{e}, cdr, n{t}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, cdr, n{y,z}>, <n{t}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{e}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{e}, cdr, n{t}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x}, car, n{y,z}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{e}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{e}, cdr, n{t}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x}, car, n{}>, <n{x}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{e}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{e}, cdr, n{t}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x,y}, car, n{}>, <n{x,y}, cdr, n{e}>, <n{t}, car, n{}>, <n{t}, cdr, n{}>, <n{e}, cdr, n{t}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
【００８３】
・データフロー方程式：
IN14 = OUT13
OUT14 = F[t := nil](IN14)
・マップ（OUT）:
OUT14：条件1.2に該当する。
Ev: <x, n{x}>, <y, n{y,z}>, <z, n{y,z}>, <x, n{x,y}>, <y, n{x,y}>, <e, n{e}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{e}>, <n{}, car, n{y,z}>, <n{}, cdr, n{y,z}>, <n{x}, car, n{y,z}>, <n{x}, cdr, n{y,z}>, <n{x,y}, car, n{}>, <n{x,y}, cdr, n{e}>, <n{e}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{e}>, <n{e}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{e}>, <n{e}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x}, car, n{y,z}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{e}>, <n{e}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x}, car, n{}>, <n{x}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{e}>, <n{e}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x,y}, car, n{}>, <n{x,y}, cdr, n{e}>, <n{e}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
【００８４】
・データフロー方程式：
IN15 = OUT14
OUT15 = F[e := nil](IN15)
・マップ（OUT）:
OUT15：条件1.2に該当する。
Ev: <x, n{x}>, <y, n{y,z}>, <z, n{y,z}>, <x, n{x,y}>, <y, n{x,y}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{y,z}>, <n{}, cdr, n{y,z}>, <n{x}, car, n{y,z}>, <n{x}, cdr, n{y,z}>, <n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x}, car, n{y,z}>, <n{x}, cdr, n{}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x}, car, n{}>, <n{x}, cdr, n{y,z}>, <n{y,z}, car, n{}>, <n{y,z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x,y}, car, n{}>, <n{x,y}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
【００８５】
・データフロー方程式：
IN16 = OUT15
OUT16 = F[y := nil](IN16)
・マップ（OUT）:
OUT16：条件1.2に該当する。
Ev: <x, n{x}>, <z, n{z}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{z}>, <n{}, cdr, n{z}>, <n{x}, car, n{z}>, <n{x}, cdr, n{z}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x}, car, n{z}>, <n{x}, cdr, n{}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x}, car, n{}>, <n{x}, cdr, n{z}>, <n{z}, car, n{}>, <n{z}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
[<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
【００８６】
・データフロー方程式：
IN17 = OUT16
OUT17 = F[z := nil](IN17)
・マップ（OUT）:
OUT17：条件1.2に該当する。
Ev: <x, n{x}>
Es: <n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>
Map: [<n{x}, car, n{}>, <n{x}, cdr, n{}>, <n{}, car, n{}>, <n{}, cdr, n{}>] -> m + 1
【００８７】
その後、どの基本ブロックに対して対応するデータフロー方程式を適用しても、マップには変化がない。即ち、不動点に到達したことになる。よって、ここで処理を終了して、この時点でのマップが答えとなる。
【００８８】
最後に、本実施の形態におけるプログラム解析装置１０を適用するのに好適なコンピュータのハードウェア構成について説明する。図１３は、このようなコンピュータのハードウェア構成の一例を示した図である。図示するように、コンピュータは、演算手段であるＣＰＵ(Central Processing Unit）９０ａと、Ｍ／Ｂ(マザーボード）チップセット９０ｂを介してＣＰＵ９０ａに接続されたメインメモリ９０ｃと、同じくＭ／Ｂチップセット９０ｂを介してＣＰＵ９０ａに接続された表示機構９０ｄとを備える。また、Ｍ／Ｂチップセット９０ｂには、ブリッジ回路９０ｅを介して、ネットワークインターフェイス９０ｆと、磁気ディスク装置（ＨＤＤ）９０ｇと、音声機構９０ｈと、キーボード／マウス９０ｉと、フレキシブルディスクドライブ９０ｊとが接続されている。
【００８９】
尚、図１３において、各構成要素は、バスを介して接続される。例えば、ＣＰＵ９０ａとＭ／Ｂチップセット９０ｂの間や、Ｍ／Ｂチップセット９０ｂとメインメモリ９０ｃの間は、ＣＰＵバスを介して接続される。また、Ｍ／Ｂチップセット９０ｂと表示機構９０ｄとの間は、ＡＧＰ（Accelerated Graphics Port）を介して接続されてもよいが、表示機構９０ｄがＰＣＩ Ｅｘｐｒｅｓｓ対応のビデオカードを含む場合、Ｍ／Ｂチップセット９０ｂとこのビデオカードの間は、ＰＣＩ Ｅｘｐｒｅｓｓ（ＰＣＩｅ）バスを介して接続される。また、ブリッジ回路９０ｅと接続する場合、ネットワークインターフェイス９０ｆについては、例えば、ＰＣＩ Ｅｘｐｒｅｓｓを用いることができる。また、磁気ディスク装置９０ｇについては、例えば、シリアルＡＴＡ（AT Attachment）、パラレル転送のＡＴＡ、ＰＣＩ（Peripheral Components Interconnect）を用いることができる。更に、キーボード／マウス９０ｉ、及び、フレキシブルディスクドライブ９０ｊについては、ＵＳＢ（Universal Serial Bus）を用いることができる。
【００９０】
ここで、本発明は、全てハードウェアで実現してもよいし、全てソフトウェアで実現してもよい。また、ハードウェア及びソフトウェアの両方により実現することも可能である。また、本発明は、コンピュータ、データ処理システム、コンピュータプログラムとして実現することができる。このコンピュータプログラムは、コンピュータにより読取り可能な媒体に記憶され、提供され得る。ここで、媒体としては、電子的、磁気的、光学的、電磁的、赤外線又は半導体システム（装置又は機器）、或いは、伝搬媒体が考えられる。また、コンピュータにより読取り可能な媒体としては、半導体、ソリッドステート記憶装置、磁気テープ、取り外し可能なコンピュータディスケット、ランダムアクセスメモリ（ＲＡＭ）、リードオンリーメモリ（ＲＯＭ）、リジッド磁気ディスク、及び光ディスクが例示される。現時点における光ディスクの例には、コンパクトディスク−リードオンリーメモリ（ＣＤ−ＲＯＭ）、コンパクトディスク−リード／ライト（ＣＤ−Ｒ／Ｗ）及びＤＶＤが含まれる。
【００９１】
以上、本発明を実施の形態を用いて説明したが、本発明の技術的範囲は上記実施の形態には限定されない。本発明の精神及び範囲から逸脱することなく様々に変更したり代替態様を採用したりすることが可能なことは、当業者に明らかである。
【図面の簡単な説明】
【００９２】
【図１】本発明の実施の形態の概要を説明するための図である。
【図２】変数xから指されたリストを表す形状グラフを示した図である。
【図３】本発明の実施の形態におけるプログラム解析装置の機能構成例を示した図である。
【図４】本発明の実施の形態におけるプログラム解析装置のメインの動作例を示したフローチャートである。
【図５】本発明の実施の形態で更新されるマップの例を示した図である。
【図６】本発明の実施の形態におけるマップ（OUT）の更新時の動作例を示したフローチャートである。
【図７】本発明の実施の形態におけるマップ（OUT）の更新時の動作例を示したフローチャートである。
【図８】本発明の実施の形態におけるマップ（OUT）の更新時の動作例を示したフローチャートである。
【図９】本発明の実施の形態におけるマップ（OUT）の更新時の動作例を示したフローチャートである。
【図１０】本発明の実施の形態におけるマップ（IN）の更新時の動作例を示したフローチャートである。
【図１１】実行例で用いたプログラムのコードを示した図である。
【図１２】実行例で用いたプログラムの制御フローグラフを示した図である。
【図１３】本発明の実施の形態を適用可能なコンピュータのハードウェア構成を示した図である。
【符号の説明】
【００９３】
１０…プログラム解析装置、１１…プログラム記憶部、１２…制御フローグラフ生成部、１３…制御フローグラフ記憶部、１４…初期マップ生成部、１５…マップ記憶部、１６…データフロー方程式生成部、１７…データフロー方程式記憶部、１８…マップ更新部
【図１】
2010020558.tif 000005
【図２】
2010020558.tif 000006
【図３】
2010020558.tif 000007
【図４】
2010020558.tif 000008
【図５】
2010020558.tif 000009
【図６】
2010020558.tif 000010
【図７】
2010020558.tif 000011
【図８】
2010020558.tif 000012
【図９】
2010020558.tif 000013
【図１０】
2010020558.tif 000014
【図１１】
2010020558.tif 000015
【図１２】
2010020558.tif 000016
【図１３】
2010020558.tif 000017