(57)【要約】      （修正有）【課題】比較的少ない処理負荷により、所定の命題を与えた場合の所定の論理式に対する全ての反例を検出することを可能とする。【解決手段】情報処理装置において、第１の論理式を、加法標準形の第２の論理式に変換する変換部１５と、変換部により変換された第２の論理式を、選言を含まない最小項に分解する分解部１６と、所定の命題に含まれる事前条件が連言節により前記最小項に追加された、第３の論理式が充足可能であり、かつ、所定の命題に含まれる事後条件が連言節により前記最小項に追加された、第４の論理式が充足可能でない場合、前記最小項を、所定の命題に対する反例であると判定する判定部１７と、を備える。【選択図】図２
2018101204.tif 000002
【特許請求の範囲】
【請求項１】
第１の論理式を、加法標準形の第２の論理式に変換する変換部と、
前記変換部により変換された前記第２の論理式を、選言を含まない最小項に分解する分解部と、
所定の命題に含まれる事前条件が連言節により前記最小項に追加された、第３の論理式が充足可能であり、かつ、前記所定の命題に含まれる事後条件が連言節により前記最小項に追加された、第４の論理式が充足可能でない場合、前記最小項を、前記所定の命題に対する反例であると判定する判定部と、
を備えることを特徴とする情報処理装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、情報処理装置に関する。
【背景技術】
【０００２】
従来、充足可能性問題（satisfiability problem, SAT）の充足可能性を判定するソフトウェアである、ＳＡＴソルバ（命題論理に対するソルバ）やＳＭＴ（Satisfiability Modulo Theories）ソルバ（述語論理に対するソルバ）を用いて、プログラムや設計の試験を行う技術が知られている（例えば、特許文献１乃至３を参照）。なお、ＳＭＴソルバはＳＡＴソルバと背景理論ソルバを組み合わせて構成されている。そのため、ＳＭＴも一階述語論理式を命題式に抽象化したうえでＳＡＴソルバによって充足可能性問題を解く方法が内包されており、これにＥＵＦ（Equality and Uninterpreted Function）など複数の背景理論ソルバを適用して問題を解いている。
【０００３】
ここで、充足可能性問題とは、論理式に含まれる変数の値に偽（Ｆａｌｓｅ）または真（Ｔｒｕｅ）を割り当てることによって、当該論理式の値を真にできるかという問題をいう。
【０００４】
従来のＳＡＴソルバやＳＭＴソルバは、ＣＮＦ（Conjunctive Normal Form、連言標準形）の論理式を用い、１つ以上のリテラル（原子論理式）の論理和を１つ以上含む論理積の形式を解くことにより、論理式の充足性を判定する。そのため、従来のＳＡＴソルバやＳＭＴソルバを用いて、所定の命題を与えた場合の所定の論理式の充足性を判定させると、１つの反例が見つかった時点で、当該所定の論理式全体の値が偽となり、他の反例を検出せずに処理を終了する。なお、反例とは、所定の命題を与えた場合に所定の論理式が充足しないリテラルのことをいう。
【０００５】
従来のＳＡＴソルバやＳＭＴソルバを用いて、所定の命題を与えた場合の所定の論理式についての全ての反例を検出する場合、既に検出された反例の否定を命題における事前条件に追加しながら、他の反例を１つずつ検出することが知られている（例えば、特許文献１を参照）。
【先行技術文献】
【特許文献】
【０００６】
【特許文献１】特許第５４６４０３１号公報
【特許文献２】特許第５３９６４０６号公報
【特許文献３】特許第５０７２８８９号公報
【発明の概要】
【発明が解決しようとする課題】
【０００７】
しかしながら、この場合、反例が検出されなくなるまで充足性を判定する処理を繰り返し行う必要がある上に、反例が検出される都度、事前条件が追加される。そのため、所定の命題を与えた場合の所定の論理式に対する全ての反例を検出する処理に時間がかかり、当該処理が有限時間内に完了しない可能性があるという問題がある。
【０００８】
そこで、上記課題に鑑み、比較的少ない処理負荷により、所定の命題を与えた場合の所定の論理式に対する全ての反例を検出できる技術を提供することを目的とする。
【課題を解決するための手段】
【０００９】
上記目的を達成するため、本発明の一実施形態に係る情報処理装置は、第１の論理式を、加法標準形の第２の論理式に変換する変換部と、前記変換部により変換された前記第２の論理式を、選言を含まない最小項に分解する分解部と、所定の命題に含まれる事前条件が連言節により前記最小項に追加された、第３の論理式が充足可能であり、かつ、前記所定の命題に含まれる事後条件が連言節により前記最小項に追加された、第４の論理式が充足可能でない場合、前記最小項を、前記所定の命題に対する反例であると判定する判定部と、を備える。
【００１０】
この情報処理装置によれば、所定の論理式を、加法標準形に変換した後、各最小項に分解し、当該最小項毎に反例を検出することにより、当該所定の論理式に対する全ての反例を検出する。
【発明の効果】
【００１１】
本実施形態によれば、比較的少ない処理負荷により、所定の命題を与えた場合の所定の論理式に対する全ての反例を検出することが可能となる。
【図面の簡単な説明】
【００１２】
【図１】実施形態に係る情報処理装置のハードウェア構成例を示す図である。
【図２】実施形態に係る情報処理装置の機能ブロック図である。
【図３】情報処理装置の処理の一例を示すフローチャートである。
【図４】解析対象のデータの一例を説明する図である。
【図５】プログラムスライシングした結果の一例を説明する図である。
【図６】依存グラフの一例を説明する図である。
【図７】一階述語論理式の一例について説明する図である。
【図８】ＤＮＦの論理式の一例について説明する図である。
【図９】分割された最小項の一例について説明する図である。
【図１０】反例となる最小項を抽出する処理の一例を示すフローチャートである。
【図１１】反例となる最小項を全て抽出する処理について説明する図である。
【図１２】反例となる最小項を全て抽出する処理について説明する図である。
【図１３】反例であると判定された最小項を含むリストの一例について説明する図である。
【発明を実施するための形態】
【００１３】
以下、図面に基づいて本発明の実施形態を説明する。図１は、実施形態に係る情報処理装置１０のハードウェア構成例を示す図である。図１の情報処理装置１０は、それぞれバスＢで相互に接続されているドライブ装置１００、補助記憶装置１０２、メモリ装置１０３、ＣＰＵ１０４、インタフェース装置１０５、表示装置１０６、及び入力装置１０７等を有する。
【００１４】
情報処理装置１０での処理を実現するプログラムは、記録媒体１０１によって提供される。プログラムを記録した記録媒体１０１がドライブ装置１００にセットされると、プログラムが記録媒体１０１からドライブ装置１００を介して補助記憶装置１０２にインストールされる。但し、プログラムのインストールは必ずしも記録媒体１０１より行う必要はなく、ネットワークを介して他のコンピュータよりダウンロードするようにしてもよい。補助記憶装置１０２は、インストールされたプログラムを格納すると共に、必要なファイルやデータ等を格納する。
【００１５】
メモリ装置１０３は、プログラムの起動指示があった場合に、補助記憶装置１０２からプログラムを読み出して格納する。ＣＰＵ１０４は、メモリ装置１０３に格納されたプログラムに従って情報処理装置１０に係る機能を実現する。インタフェース装置１０５は、ネットワークに接続するためのインタフェースとして用いられる。表示装置１０６はプログラムによるＧＵＩ（Graphical User Interface）等を表示する。入力装置１０７はキーボード及びマウス等、またはタッチパネル及びボタン等で構成され、様々な操作指示を入力させるために用いられる。
【００１６】
なお、記録媒体１０１の一例としては、ＣＤ−ＲＯＭ、ＤＶＤディスク、又はＵＳＢメモリ等の可搬型の記録媒体が挙げられる。また、補助記憶装置１０２の一例としては、ＨＤＤ（Hard Disk Drive）又はフラッシュメモリ等が挙げられる。記録媒体１０１及び補助記憶装置１０２のいずれについても、コンピュータ読み取り可能な記録媒体に相当する。
【００１７】
次に、図２を参照し、情報処理装置１０の機能構成について説明する。図２は、情報処理装置１０の機能ブロック図である。情報処理装置１０は、取得部１１、プログラムスライシング部１２、依存グラフ分析部１３、一階述語論理式生成部１４、加法標準形論理式変換部１５、分解部１６、及び判定部１７を備える。これら各部は、情報処理装置１０にインストールされた１以上のプログラムが、情報処理装置１０のＣＰＵ１０４に実行させる処理により実現される。
【００１８】
取得部１１は、例えばユーザにより予め設定された、解析対象のデータを取得する。ここで、解析対象のデータは、例えば、準形式手法記述モデルに従った設計データ、または所定のプログラムのソースコード等である。
【００１９】
また、取得部１１は、例えばユーザからの入力操作等により予め指定された、所定の命題を取得する。なお、命題とは、事前条件が成り立てば、事後条件が成り立つということを示す情報である。そのため、命題には、事前条件、及び事後条件の情報が含まれる。
【００２０】
プログラムスライシング部１２は、取得部１１により取得された解析対象のデータに基づいて、プログラムスライシングを行う。ここで、プログラムスライシングとは、設計データまたはプログラム内の所定の変数（処理）に影響を与える処理のみを、当該設計データまたは当該プログラムから抽出する処理である。なお、プログラムスライシングは、公知の技術を用いて行ってもよい。
【００２１】
依存グラフ分析部１３は、プログラムスライシング部１２によるプログラムスライシングの結果に基づいて、依存グラフを生成する。ここで、依存グラフとは、例えば、所定の変数の出力に至る各演算経路（処理経路）と、処理等との関係、及び各演算経路における分岐の条件等を示すデータである。なお、依存グラフを生成する処理は、公知の技術を用いて行ってもよい。
【００２２】
一階述語論理式生成部１４は、依存グラフ分析部１３により生成された依存グラフを、一階述語論理式（「第１の論理式」の一例）に変換する。なお、一階述語論理式生成部１４は、依存グラフを一階述語論理式に変換する処理を、公知の技術を用いて行ってもよい。なお、一階述語論理式生成部１４は、解析対象のデータ等に基づいて、他の公知の手法に基づいて一階述語論理式を生成してもよい。
【００２３】
加法標準形論理式変換部１５は、当該一階述語論理式を、論理演算の法則を用いて、ＤＮＦ（Disjunctive normal form）の論理式（「第２の論理式」の一例）に変換する。なお、ＤＮＦとは、１つ以上のリテラルの論理積を１つ以上含む論理和の形式であり、「加法標準形」、「選言標準形」等とも称される。当該一階述語論理式からＤＮＦの論理式への変換は、二重否定の除去、ド・モルガンの法則、分配法則といった論理的に等価な変換を行う論理演算の法則を用いて変換できる。
【００２４】
分解部１６は、加法標準形論理式変換部１５により生成されたＤＮＦの論理式を、選言（ＯＲ）を含まない、連言節（ＡＮＤ）で表される項である最小項毎に分解する。
【００２５】
判定部１７は、分解部１６により分解された各最小項について、取得部１１により取得された所定の命題に対する反例であるか否かを判定し、分解された各最小項のうち、当該反例となる最小項を全て抽出する。なお、反例とは、所定の命題における事前条件が成り立つ場合でも、当該所定の命題における事後条件が成り立たない場合であることを示す。
【００２６】
判定部１７は、分散処理部１７１、背景理論検証部１７２、及び集約部１７３を備える。
【００２７】
分散処理部１７１は、所定の命題に含まれる事前条件と前記最小項の論理とが矛盾せず、かつ、前記所定の命題に含まれる事後条件と前記最小項の論理とが矛盾する場合、前記最小項を、前記命題に対する反例であると判定する。
【００２８】
より具体的には、分散処理部１７１は、所定の命題に含まれる事前条件が連言節により最小項に追加された、第３の論理式が充足可能であるか否かを判定する。そして、分散処理部１７１は、第３の論理式が充足可能である場合、当該所定の命題に含まれる事後条件が連言節により当該最小項に追加された第４の論理式が充足可能であるか否かを判定する。そして、分散処理部１７１は、第３の論理式が充足可能であり、かつ、第４の論理式が充足可能でない場合、当該最小項を、当該所定の命題に対する反例であると判定する。なお、所定の論理式が「充足可能」であるとは、当該所定の論理式に含まれる変数の値に偽（Ｆａｌｓｅ）または真（Ｔｒｕｅ）を割り当てることによって、当該所定の論理式の値を真にできる場合があることをいう。例えば、検証対象の論理式において、変数ａが変数ｂと等しく、かつ、変数ａが変数ｂと等しないという式（（ａ＝＝ｂ）∧（ａ！＝ｂ））が含まれる場合、当該論理式は矛盾し、変数ａと変数ｂにいかなる真偽値を代入しても当該論理式は偽になるため、充足可能でない（充足不能）と判定される。
【００２９】
分散処理部１７１は、分解部１６により分解された各最小項について、当該反例であるか否かを判定する処理を、例えば並列分散処理により実行する。
【００３０】
背景理論検証部１７２は、分散処理部１７１に指示に応じて、所定の論理式について、背景理論検証の処理を行う。なお、背景理論検証は、公知の背景理論ソルバを用いてもよい。背景理論検証において、予め設定されている情報等に基づき、検証対象の論理式が充足可能であるか否かが判定される。
【００３１】
集約部１７３は、分散処理部１７１により反例であると判定された最小項を含むリストを生成する。
【００３２】
＜処理＞
次に、図３を参照し、情報処理装置１０による処理について説明する。図３は、情報処理装置の処理の一例を示すフローチャートである。
【００３３】
ステップＳ１において、取得部１１は、解析対象のデータを取得する。
【００３４】
図４は、解析対象のデータの一例を説明する図である。図４では、処理「ａ」５０１乃至処理「ｎ」５１４間の入出力の関係が規定されている。処理「ａ」５０１乃至処理「ｎ」５１４では、それぞれ、例えば少数、整数、文字列等の型のデータを用いて、任意の処理が行われ、任意の型のデータが出力される。図４における矢印は、矢印の元からの出力データが、矢印の先に入力されることを示している。
【００３５】
そのため、図４の例では、例えば処理「ｆ」５０６は、処理「ｅ」５０５及び処理「ａ」５０１の結果により出力されたデータを入力し、処理「ｆ」５０６に応じた所定の処理を行い、処理結果のデータをスイッチ５５１及びスイッチ５５２に出力する。
【００３６】
スイッチ５５１乃至スイッチ５５６は分岐を示す。各スイッチの左端中央部分５５１ａ乃至５５６ａは、分岐の条件を示し、例えばＣ言語によるソースコードにおけるｉｆ文の条件に相当する。図４の例では、当該ｉｆ文の結果が真（ｔｒｕｅ）であれば、左端上側部分５５１ｂ乃至５５６ｂから入力されたデータが出力され、当該ｉｆ文の結果が偽（ｆａｌｓｅ）であれば、左端下側部分５５１ｃ乃至５５６ｃから入力されたデータが出力されるものとする。なお、図４のようなデータは、公知のツール等を用いて作成できる。
【００３７】
続いて、プログラムスライシング部１２は、解析対象のデータに基づいて、プログラムスライシングを行う（ステップＳ２）。
【００３８】
続いて、依存グラフ分析部１３は、プログラムスライシングの結果に基づいて、依存グラフを生成する（ステップＳ３）。
【００３９】
図５及び図６を参照し、プログラムスライシング及び依存グラフについて説明する。図５は、プログラムスライシングした結果の一例を説明する図である。図５では、図４の解析対象のデータをプログラムスライシングした結果において、例えば、図４の処理「ｊ」５１０が指定され、処理「ｊ」５１０に至る演算経路が抽出された例を示す。図５では、図４と比較して、処理「ｊ」５１０と無関係な処理「ｋ」５１１に至る演算経路が取り除かれている。図５の演算経路６０１乃至演算経路６１３は、依存グラフにおける演算経路のインデックスを示す。
【００４０】
図６は、依存グラフの一例を説明する図である。図６では、図５の演算経路６０１乃至演算経路６１３と、図５の処理「ａ」５０１乃至処理「ｊ」５１０との関係、及び各演算経路における分岐の条件が示されている。
【００４１】
続いて、一階述語論理式生成部１４は、依存グラフを、一階述語論理式に変換する（ステップＳ４）。
【００４２】
図７は、一階述語論理式の一例について説明する図である。図７では、図６の依存グラフに対する一階述語論理式の例を示す。図７では、処理「ｊ」５１０に、処理「ｅ」５０５、処理「ｇ」５０７、処理「ｈ」５０８の出力結果が入力される場合の論理式が生成されている。図７において、ｆ（ｘ、ｙ）は、処理「ｆ」に処理「ｘ」及び処理「ｙ」の出力結果が入力されることを表す。「∧」はＡＮＤ条件、「∨」はＯＲ条件を表す。「ｘ＝＝ｙ」は、ｘとｙが一致することを表す。
【００４３】
続いて、加法標準形論理式変換部１５は、当該一階述語論理式を、論理演算の法則を用いて、ＤＮＦ（Disjunctive normal form）の論理式に変換する（ステップＳ５）。
【００４４】
図８は、ＤＮＦの論理式の一例について説明する図である。図８では、図７の一階述語論理式に対するＤＮＦの論理式の例を示す。図８における記号の意味は、図７における記号の意味と同様である。なお、図８に示すＤＮＦの論理式と、図７に示す一階述語論理式とは、論理的に等価である。
【００４５】
続いて、分解部１６は、当該ＤＮＦの論理式を、選言（ＯＲ）を含まない、連言節（ＡＮＤ）で表される項（最小項）毎に分解する（ステップＳ６）。
【００４６】
図９は、分割された最小項の一例について説明する図である。図９では、図８に示すＤＮＦの論理式において、連言節（ＡＮＤ）で表される最小項毎に分割し、ＩＤを付加したリストの例を示している。
【００４７】
続いて、判定部１７は、分解された各最小項について、所定の命題に対する反例であるか否かを判定し、分解された各最小項のうち、当該反例となる最小項を全て抽出する（ステップＳ７）。
【００４８】
次に、図１０を参照し、ステップＳ７の、反例となる最小項を全て抽出する処理について説明する。図１０は、反例となる最小項を抽出する処理の一例を示すフローチャートである。なお、図１０では、分解された各最小項のうちの一の最小項（以下、「対象の最小項」という。）についての処理を説明するが、他の最小項についても同様の処理が実行される。なお、以下で説明する図１０に示す処理は、各最小項について並列に処理することにより、比較的高速に実行できる。
【００４９】
ステップＳ１０１において、分散処理部１７１は、指定された所定の命題における事前条件の論理式を、対象の最小項のＤＮＦの論理式に追加した論理式を生成する。
【００５０】
続いて、分散処理部１７１は、生成した論理式について、背景理論検証の処理を背景理論検証部１７２に実行させる（ステップＳ１０２）。
【００５１】
続いて、分散処理部１７１は、背景理論検証部１７２による背景理論検証の結果、当該論理式が充足可能であるか否かを判定する（ステップＳ１０３）。
【００５２】
充足可能でない場合（ステップＳ１０３でＮＯ）、分散処理部１７１は、対象の最小項は「事前条件制約外」であると判定し（ステップＳ１０４）、処理を終了する。なお、「事前条件制約外」は、事前条件を満たさないことを示す。
【００５３】
充足可能である場合（ステップＳ１０３でＹＥＳ）、分散処理部１７１は、指定された命題における事後条件の論理式を、対象の最小項のＤＮＦの論理式に追加した論理式を生成する（ステップＳ１０５）。
【００５４】
続いて、分散処理部１７１は、ステップＳ１０５で生成した論理式について、背景理論検証の処理を背景理論検証部１７２に実行させる（ステップＳ１０６）。
【００５５】
続いて、分散処理部１７１は、背景理論検証部１７２による背景理論検証の結果が充足可能であるか否かを判定する（ステップＳ１０７）。
【００５６】
充足可能である場合（ステップＳ１０７でＹＥＳ）、分散処理部１７１は、対象の最小項は「命題合致」であると判定し（ステップＳ１０８）、処理を終了する。「命題合致」は、事前条件が成り立てば、事後条件が成り立つことを示す。
【００５７】
充足可能でない場合（ステップＳ１０７でＮＯ）、分散処理部１７１は、対象の最小項は「反例」であると判定し（ステップＳ１０９）、処理を終了する。「反例」は、事前条件が成り立っている場合でも、事後条件が成り立たない場合であることを示す。
【００５８】
次に、図１１及び図１２を参照し、ステップＳ７の、反例となる最小項を全て抽出する処理について説明する。図１１及び図１２は、反例となる最小項を全て抽出する処理について説明する図である。図１１及び図１２では、命題として、「処理「ａ」５０１及び処理「ｂ」５０２からの出力に基づく分岐の条件判定の結果が真（ｔｒｕｅ）の場合、処理「ｊ」５１０に処理「ｇ」５０９から出力されたデータが入力される。」ことが指定された場合の例を説明する。
【００５９】
ステップＳ１０１の処理により、図１１に示すように、図９に示す各最小項に、命題の事前条件を示す（ａ（）＝＝ｔｒｕｅ）∧（ｂ（）＝＝ｔｒｕｅ）の論理式が追加された論理式がそれぞれ生成される。そして、ステップＳ１０３の処理により、背景理論検証の結果、各論理式が充足可能であるか充足不能であるかが判定される。例えば、図１１のＩＤが「１」及び「２」の論理式の場合、当該論理式に含まれる（ｂ（）＝＝ｆａｌｓｅ）と、（ｂ（）＝＝ｔｒｕｅ）とが矛盾するため、充足不能と判定される。図１１のＩＤが「３」の論理式の場合、矛盾がないため、充足可能と判定される。
【００６０】
そして、図１２に示すように、充足不能と判定された論理式の基となる最小項は、ステップＳ１０４の処理により、「事前条件制約外」とされる。
【００６１】
一方、充足可能と判定された論理式の基となる最小項は、ステップＳ１０５の処理により、図９に示す各最小項に、命題の事前条件を示す（ｊ＝＝ｇ（））の論理式が追加された論理式がそれぞれ生成される。そして、ステップＳ１０７の処理により、背景理論検証の結果、各論理式が充足可能であるか充足不能であるかが判定される。
【００６２】
例えば、図１２のＩＤが「３」及び「７」の論理式の場合、当該論理式に含まれる（ｊ＝＝ｅ（））と、（ｊ＝＝ｇ（））とが矛盾するため、充足不能と判定される。図１１のＩＤが「１３」の論理式の場合、矛盾がないため、充足可能と判定される。
【００６３】
そして、充足不能と判定された論理式の基となる最小項は、ステップＳ１０８の処理により、「命題合致」とされる。一方、充足不能と判定された論理式の基となる最小項は、ステップＳ１０９の処理により、「反例」とされる。
【００６４】
次に、図１３を参照し、集約部１７３により生成される、反例であると判定された最小項を含むリストについて説明する。図１３は、反例であると判定された最小項を含むリストの一例について説明する図である。
【００６５】
集約部１７３は、図１０の処理の結果に基づいて、各最小項のＩＤ応じた検証結果のリストを作成する。例えば、ユーザは、当該リストのデータを参照することにより、「反例」とされたＩＤ「３」、「７」、「９」について、命題を満たさない演算経路であることが分かるため、当該「反例」とされた演算経路に応じたテストケースを作成することができる。これにより、例えば、処理「ｊ」５１０に、処理「ｇ」５０９から出力されたデータが入力される場合以外のケースについてもテストできる。
【００６６】
＜まとめ＞
従来技術では、所定の命題を与えた場合の所定の論理式に対する全ての反例を検出する処理に時間がかかるという問題がある。
【００６７】
上述した実施形態によれば、加法標準形に変換された論理式を、選言を含まない最小項に分解し、所定の命題における事前条件を満たし、当該所定の命題における事後条件を満たさない最小項を反例であると判定する。これにより、比較的少ない処理負荷により、所定の命題を与えた場合の所定の論理式に対する全ての反例を検出することができる。また、全ての反例を検出することにより、各反例における分岐条件及び演算経路が分かるため、プログラムのバグや設計や仕様の誤りを検出するためのテストケースの作成に役立てることができる。それによりテストケースの作成等にかかる時間を短縮できる。
【００６８】
以上、本発明の実施例について詳述したが、本発明は斯かる特定の実施形態に限定されるものではなく、特許請求の範囲に記載された本発明の要旨の範囲内において、種々の変形・変更が可能である。
【００６９】
情報処理装置１０の各機能部は、例えば１以上のコンピュータにより構成されるクラウドコンピューティングにより実現されていてもよい。
【符号の説明】
【００７０】
１０  情報処理装置
１１  取得部
１２  プログラムスライシング部
１３  依存グラフ分析部
１４  一階述語論理式生成部
１５  加法標準形論理式変換部（変換部）
１６  分解部
１７  判定部
１７１  分散処理部
１７２  背景理論検証部
１７３  集約部
【図１】
2018101204.tif 000003
【図２】
2018101204.tif 000004
【図３】
2018101204.tif 000005
【図４】
2018101204.tif 000006
【図５】
2018101204.tif 000007
【図６】
2018101204.tif 000008
【図７】
2018101204.tif 000009
【図８】
2018101204.tif 000010
【図９】
2018101204.tif 000011
【図１０】
2018101204.tif 000012
【図１１】
2018101204.tif 000013
【図１２】
2018101204.tif 000014
【図１３】
2018101204.tif 000015