(57)【要約】【課題】膨大な作業量・記憶領域を必要とすることなくプロパティを適正に修正すること。【解決手段】反例に加え、正例とそれに対応するプロパティを利用する。具体的には、反例と正例の差分をとる。また、正例側あるいは反例側の差分状態遷移列で用いられているプロパティ中の条件を、不足条件の候補として利用する。これにより、正例と反例の正例側差分状態遷移列中で駆動されたイベントに関するプロパティから正例の維持と反例のガードという修正対象プロパティの事前条件不足解消の要件を満たす条件を生成・追加することで、プロパティの事前条件が修正可能になる。【選択図】図１
2010282257.tif 000002
【特許請求の範囲】
【請求項１】
検査対象プログラムの設計上の性質・仕様を、該検査対象プログラムにおいて駆動されるイベントごとに、論理式で定義される事前条件と事後条件によって記述したプロパティについて、該プロパティの記述の誤りを修正するためのプログラムであって、
前記検査対象プログラムの実行によって、事前条件が真で事後条件が偽となったイベントに係るプロパティを、修正対象プロパティとして取得する取得手段と、
前記検査対象プログラムの初期状態から前記修正対象プロパティに係るイベントに到るまでに駆動された全イベントを特定する情報を含む状態遷移列を反例として検出するとともに、該検査対象プログラムの実行によって駆動された該修正対象プロパティに係るイベントと同一のイベントのうち、事前条件と事後条件とが共に真となったイベントを特定し、該初期状態から該特定されたイベントに到るまでに駆動された全イベントを特定する情報を含む状態遷移列を該反例に対する正例として検出する検出手段と、
前記検出手段によって検出された前記反例および前記正例の差分のイベントを特定する情報を含む差分状態遷移列を抽出する差分抽出手段と、
前記差分抽出手段によって抽出された前記差分状態遷移列に含まれるイベントに係るプロパティの前記事前条件および前記事後条件を論理積標準形に変換し、変換後の該事前条件および該事後条件に含まれる各節の論理式を、差分論理式として抽出する差分論理式抽出手段と、
前記差分論理式抽出手段によって抽出された前記差分論理式の真偽判定を、前記正例の最終のイベントの駆動元の状態と、前記反例の最終のイベントの駆動元の状態それぞれに基づいて行い、真偽判定結果が前記正例の最終のイベントの駆動元の状態と前記反例の最終のイベントの駆動元の状態とで異なる場合に、該差分論理式を候補論理式として生成する生成手段と、
前記生成手段によって生成された候補論理式を前記修正対象プロパティの事前条件に追加することにより、修正済プロパティを生成する修正手段と、
前記修正手段によって修正された修正済プロパティを出力する出力手段、
としてコンピュータを機能させることを特徴とするプロパティ修正プログラム。
【請求項２】
前記修正手段は、
前記生成手段において、前記候補論理式の真偽判定結果が、前記正例の最終のイベントの駆動元の状態では偽で、かつ、前記反例の最終のイベントの駆動元の状態では真である場合、前記候補論理式の否定を前記修正対象プロパティの事前条件に追加することにより、修正済プロパティを生成することを特徴とする請求項１に記載のプロパティ修正プログラム。
【請求項３】
前記検出手段は、前記正例を複数検出し、
前記差分抽出手段は、前記複数の正例の中から選ばれた一の正例と前記反例との差分となる差分状態遷移列を抽出することを特徴とする請求項１または２に記載のプロパティ修正プログラム。
【請求項４】
前記差分論理式抽出手段は、論理積標準形への変換後の前記事前条件および事後条件に含まれる各節の論理式、および、該各節の部分節の論理式を差分論理式として抽出する請求項１，２または３に記載のプロパティ修正プログラム。
【請求項５】
検査対象プログラムの設計上の性質・仕様を、該検査対象プログラムにおいて駆動されるイベントごとに、論理式で定義される事前条件と事後条件によって記述したプロパティについて、該プロパティの記述の誤りを修正するための装置であって、
前記検査対象プログラムの実行によって、事前条件が真で事後条件が偽となったイベントに係るプロパティを、修正対象プロパティとして取得する取得手段と、
前記検査対象プログラムの初期状態から前記修正対象プロパティに係るイベントに到るまでに駆動された全イベントを特定する情報を含む状態遷移列を反例として検出するとともに、該検査対象プログラムの実行によって駆動された該修正対象プロパティに係るイベントと同一のイベントのうち、事前条件と事後条件とが共に真となったイベントを特定し、該初期状態から該特定されたイベントに到るまでに駆動された全イベントを特定する情報を含む状態遷移列を該反例に対する正例として検出する検出手段と、
前記検出手段によって検出された前記反例および前記正例の差分のイベントを特定する情報を含む差分状態遷移列を抽出する差分抽出手段と、
前記差分抽出手段によって抽出された前記差分状態遷移列に含まれるイベントに係るプロパティの前記事前条件および前記事後条件を論理積標準形に変換し、変換後の該事前条件および該事後条件に含まれる各節の論理式を、差分論理式として抽出する差分論理式抽出手段と、
前記差分論理式抽出手段によって抽出された前記差分論理式の真偽判定を、前記正例の最終のイベントの駆動元の状態と、前記反例の最終のイベントの駆動元の状態それぞれに基づいて行い、真偽判定結果が前記正例の最終のイベントの駆動元の状態と前記反例の最終のイベントの駆動元の状態とで異なる場合に、該差分論理式を候補論理式として生成する生成手段と、
前記生成手段によって生成された候補論理式を前記修正対象プロパティの事前条件に追加することにより、修正済プロパティを生成する修正手段と、
前記修正手段によって修正された修正済プロパティを出力する出力手段と、
を備えることを特徴とするプロパティ修正装置。
【請求項６】
検査対象プログラムの設計上の性質・仕様を、該検査対象プログラムにおいて駆動されるイベントごとに、論理式で定義される事前条件と事後条件によって記述したプロパティについて、該プロパティの記述の誤りを修正するための方法であって、
前記検査対象プログラムの実行によって、事前条件が真で事後条件が偽となったイベントに係るプロパティを、修正対象プロパティとして取得する取得工程と、
前記検査対象プログラムの初期状態から前記修正対象プロパティに係るイベントに到るまでに駆動された全イベントを特定する情報を含む状態遷移列を反例として検出するとともに、該検査対象プログラムの実行によって駆動された該修正対象プロパティに係るイベントと同一のイベントのうち、事前条件と事後条件とが共に真となったイベントを特定し、該初期状態から該特定されたイベントに到るまでに駆動された全イベントを特定する情報を含む状態遷移列を該反例に対する正例として検出する検出工程と、
前記検出工程によって検出された前記反例および前記正例の差分のイベントを特定する情報を含む差分状態遷移列を抽出する差分抽出工程と、
前記差分抽出工程によって抽出された前記差分状態遷移列に含まれるイベントに係るプロパティの前記事前条件および前記事後条件を論理積標準形に変換し、変換後の該事前条件および該事後条件に含まれる各節の論理式を、差分論理式として抽出する差分論理式抽出工程と、
前記差分論理式抽出工程によって抽出された前記差分論理式の真偽判定を、前記正例の最終のイベントの駆動元の状態と、前記反例の最終のイベントの駆動元の状態それぞれに基づいて行い、真偽判定結果が前記正例の最終のイベントの駆動元の状態と前記反例の最終のイベントの駆動元の状態とで異なる場合に、該差分論理式を候補論理式として生成する生成工程と、
前記生成工程によって生成された候補論理式を前記修正対象プロパティの事前条件に追加することにより、修正済プロパティを生成する修正工程と、
前記修正工程によって修正された修正済プロパティを出力する出力工程と、
をコンピュータが実行することを特徴とするプロパティ修正方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本開示技術は、反例を解析するプロパティ修正プログラム、プロパティ修正装置、およびプロパティ修正方法に関する。
【背景技術】
【０００２】
従来、プログラムソースコードやハードウェア記述言語（ＨＤＬ）によるハードウェア設計記述の修正方法として、設計規約等をルール化した雛形に従った記述修正の技術が広く用いられている。たとえば、下記特許文献１ではソースコードを自社のルール（雛形）に従って修正する技術が開示されている。
【０００３】
また、下記特許文献２ではソースコードをルール（雛形）に従って修正後、修正後のソースコードから得た実行ファイルに対してテストを実施し妥当性を検証する技術が開示されている。さらに、下記特許文献３ではＨＤＬの意味論的文法違反となるデータ型不整合や不適切な設計記述を言語変換規則という雛形を用いて変換する技術が開示されている。
【０００４】
本開示技術の適用先の一つであるプログラムモデル検査とは、検査対象のプログラムが満たすべき設計上の性質・仕様を定義したプロパティを満たしているかを、プログラムを網羅的に実行して検査することである。網羅的な実行とは、プログラムを整合的に実行するあらゆる状態遷移列を再現し、実行することである。
【０００５】
前記プロパティは、論理式の形式で記述され、たとえば、あるイベント（キー入力やマウス操作などのユーザによって実行された動作）に対して、“Ａ−＞Ｂ”（イベントがＡの条件で駆動したら、Ｂの状況になる）の形式で記述される。部分論理式は、プログラムの変数に関係演算を適用した項（プログラム変数に関する述語）を論理的に組み合わせた論理式である。下記部分論理式Ｃは、「画面．商品ＩＤ！＝０」の項と「画面．合計＞１０００」の項とを論理的に組み合わせた論理式である。
【０００６】
Ｃ＝（画面．商品ＩＤ！＝０）ａｎｄ（画面．合計＞１０００）
【０００７】
プログラムモデル検査結果を利用したプログラムおよびプロパティ修正の一例として反例解析がある。反例解析とは、反例（プロパティが偽となる状態と、初期状態からその状態への状態遷移列）を使って、プログラムおよびプロパティの修正方法を解析することである。なお、状態とは、全プログラム変数の実際の値の集まりである。
【０００８】
また、プロパティにおいて、事前条件とは、事後条件が成立するための十分条件である。すなわち、事前条件が成立するならば事後条件が必ず成立することとなる。たとえば、下記プロパティＰの場合、サービス対象となるような条件は、「商品ＩＤが空ではなくて、合計が１０００以上」となり、それ以外の変数に関するものを含め、別の条件は関係してこない。
【０００９】
Ｐ：＝（画面．商品ＩＤ！＝“”）ａｎｄ（画面．合計＞１０００）−＞（ＤＢ．サービス対象＝＝ｔｒｕｅ）
【００１０】
各プロパティは、評価対象のイベント実施前後で以下の通り評価される。
［評価１］各プロパティは、評価対象のイベント駆動直前のプログラム状態が事前条件を満たし、かつ当該評価対象のイベント駆動直後のプログラム状態が事後条件を満たしていれば、当該評価対象のイベントに関して成立する。
【００１１】
［評価２］各プロパティは、評価対象のイベント駆動直前のプログラム状態が事前条件を満たしており、かつ当該評価対象のイベント駆動直後のプログラム状態が事後条件を満たしていなければ、当該評価対象のイベントに関して違反する（成立しない）。
【００１２】
［評価３］各プロパティは、評価対象のイベント駆動直前のプログラム状態が事前条件を満たしていなければ、当該評価対象のイベント駆動直後のプログラム状態が事後条件を満たしているかどうかに関わらず、当該評価対象のイベントに関して成立する。なお、特別な断りが無い限り、本明細書において、プロパティが真と評価されるとは［評価１］の通りにプロパティが評価されることを指すものとする。また、同様に特別な断りが無い限り、本明細書において、プロパティが偽と評価されるとは、［評価２］の通りにプロパティが評価されることを指すものとする。
【００１３】
一般的なモデル検査では、検査対象のプログラム実行中に検査するプロパティのどれか１つでも［評価２］の通りに評価されるものがあればプロパティ違反が発生したと判定してプログラム実行を停止する。そして、［評価２］の通り評価されたプロパティすべてを違反プロパティとして出力する。また、同時に検査開始時のプログラム状態（初期状態）からプロパティ違反が発生するまでに駆動したイベントおよび駆動イベント前後のプログラム状態からなるプログラム状態遷移を反例として出力する。
【００１４】
モデル検査の結果、プロパティ違反が発生して違反プロパティと反例を得た後、ユーザは違反プロパティと反例を元にプログラムの修正を試みる。修正を試みた結果プログラムに誤りのないことが判明した場合には、プログラムの修正ではなく違反プロパティの修正を試みることになる。また、各プロパティは基本的には独立したものであるので、違反プロパティを修正するにあたっては、当該違反プロパティを構成する各プロパティを独立に修正することができる。よって違反プロパティの中から修正対象プロパティを１つ選び修正する状況を想定する。
【００１５】
修正対象プロパティの修正にあたっては、多くの場合は事前条件を修正することになる。なぜなら、一般的に事後条件は、アプリケーションの画面の振る舞いをはじめとして、設計者が意識しやすい条件であるからである。これに対し、事前条件は、アプリケーションの画面の振る舞いに加え、設計者の意識から漏れることの多いデータベースの状態やエラー情報等の内部パラメータに関する条件が加味されるからである。
【００１６】
事前条件に対する内部パラメータに関する条件の抜けは特に頻発する傾向がある。それゆえ、抜けている条件を発見して事前条件に付加することで修正対象プロパティを修正する手法がプロパティ修正に寄与するところは大きい。たとえば、プロパティＰが偽（プロパティＰの事前条件が真で、プロパティＰの事後条件が偽）となってしまう場合、プロパティＰの事前条件が不足している可能性がある（事前条件不足の可能性）。すなわち、プロパティＰが偽である場合、プロパティＰの事前条件に出現しなかった変数に関するものを含め、出現したもの以外の条件が本来プロパティＰの事前条件で加味されるべきものとなっている可能性がある。
【００１７】
このような、事前条件不足を解消するためには、事前条件に不足条件（述語）を追加した修正を実施する必要がある。また、事前条件不足解消によって新たに反例が得られる場合についても対処する必要がある。
【００１８】
図３９は、事前条件不足解消前後を示す説明図である。図３９中、左側の図は、事前条件不足解消前のプログラム状態遷移を示しており、右側の図は、事前条件不足解消後のプログラム状態遷移を示している。また、図３９中、○図形は状態を示しており、矢印は遷移を示している。事前条件不足を解消するための要件は以下のとおりである。
【００１９】
要件の１つとしては、検証中、「プロパティＰの事前条件が真で、プロパティＰの事後条件が偽」であることが無くなることである。具体的には、状態Ｓ１のように、事前条件不足解消前では、事前条件が真で事後条件が偽となる反例が現れているが、事前条件も偽になることで、反例ではなくなる。これを「反例（の）ガード」と呼ぶ。
【００２０】
反例のガードでは、修正対象プロパティに関する反例において修正対象プロパティが［評価２］の通りに評価されたイベント駆動前後で、修正済プロパティが［評価３］の通りに評価される。なお、事後条件は修正されないため、当該イベント駆動直後のプログラム状態に関して修正済プロパティの事後条件は満たされない。ゆえに、実際には事前条件のみを修正した場合、修正済プロパティは当該イベント駆動前後で［評価１］の通りに評価されることはない。
【００２１】
もう１つの要件としては、「プロパティＰの事前条件が真かつプロパティＰの事後条件が真」であった状態遷移列において、修正後の事前条件が偽となることがないことである。具体的には、状態Ｓ２のように、事前条件不足解消前後において、事前条件および事後条件がともに真を維持している。これを「正例（の）維持」と呼ぶ。
【００２２】
正例の維持では、修正対象プロパティが［評価２］の通り評価されたイベント駆動前後では修正済プロパティが［評価２］の通りに評価される。事後条件は修正されないため、当該イベント駆動前のプログラム状態に関しても当該修正後の事前条件が成立するように事前条件を補う。なお、モデル検査の初期状態から［評価２］の通りに修正対象プロパティが評価されるイベントまでのすべての駆動イベントおよび駆動イベント前後のプログラム状態からなるプログラム状態遷移を、正例とよぶ。
【００２３】
また、状態Ｓ１での事前条件不足解消によりあらたに反例が得られた場合、新たな反例については、プログラムのミスかプロパティの不備かを改めて判定することとする。たとえば、状態Ｓ３については、事前条件不足解消前では事前条件および事後条件がともに偽であるにもかかわらず、状態Ｓ１での事前条件不足解消により、事前条件が真に遷移している。これを、「新たな反例の出現」と呼ぶ。
【００２４】
このような事前条件不足解消に基づくプロパティ修正のための方法として、従来技術における雛形の概念を踏まえ、例えば抜けている条件の候補となる条件式の雛形を利用するプログラムモデル検査手法（以下、従来手法）が考えられる。
【００２５】
図４０は、従来手法を示す説明図である。ここで、条件式の雛形とは、「整数Ｘより整数Ｙが大きい」といった、条件式の一部がパラメータ化された条件である。また、同時に「文字列Ｘの文字列長」といった条件式の雛形中のパラメータに代入することが可能な雛形関数も含む。従来手法においては、あらかじめ条件式の雛形を複数格納した述語テンプレートテーブルおよび関数テンプレートテーブルを用意した上で以下の手順でプロパティ修正を実施する。なお、修正対象プロパティは図４０のＰ１である。
【００２６】
修正対象プロパティＰ１のうち「（画面．商品ＩＤ！＝“”）ａｎｄ（画面．合計＞１０００）」が事前条件であり、「（ＤＢ．サービス対象＝＝ｔｒｕｅ）」が事後条件である。
【００２７】
（１）まず、反例においてプロパティ違反が発生したイベントを駆動する直前のプログラム状態を取得する。（２）つぎに、取得したプログラム状態を構成する変数およびその値を取り出す。ここでは、例として、｛画面．会員種別、正社員｝を取り出す。そして、あらかじめ作成された述語テンプレートテーブル上の条件式の雛形を選び、選んだ雛形のパラメータを取得変数あるいは関数テンプレートテーブル上の関数で置き換える。
【００２８】
ここでは、例として、テンプレートと引数型が｛（Ｘ！＝Ｙ）、Ｘ：文字列，Ｙ：文字列｝である条件式の雛形を選び置き換える。置き換えることにより、取得変数とその値が｛画面．会員種別！＝正会員｝となり、述語として作成される。作成された述語は、事前条件として追加される。これにより、修正対象プロパティＰ１が修正済みプロパティＰ２となる。
【００２９】
修正済みプロパティＰ２の事前条件では、作成された述語が追加されるため、「（画面．商品ＩＤ！＝“”）ａｎｄ（画面．合計＞１０００）ａｎｄ（画面．会員種別！＝正会員）」となる。なお、関数テンプレートテーブル上の関数で当該雛形のパラメータを置き換えた場合には、当該関数のパラメータを取得変数あるいは再帰的に関数テンプレートテーブル上の関数で置き換える。（３）このあと、修正済みプロパティＰ２について、実際に反例がガードされ、さらに正例が維持されていることを確認する。
【００３０】
このように、当該条件式の雛形のパラメータを置換して得た条件式を当該修正対象プロパティＰ１の事前条件に付加した修正事前条件が、プロパティ違反イベント駆動直前のプログラム状態で成立しないことを確認する。また、修正対象プロパティが［評価１］の通り評価されたイベントが存在すれば当該イベント駆動直前のプログラム状態で修正事前条件が成立していることを確認する。さらに、いずれも事前条件不足の条件を満たしているならば、修正事前条件で修正対象プロパティの事前条件を置き換えたプロパティを修正済プロパティとする。
【００３１】
上述したように、正例を維持しながら反例をガードすることで、必要かつ最小限なプロパティ修正を実現するという考え方は、最弱事前条件という概念に基づくものであり、プロパティ修正の方法として妥当といえる。また、修正済プロパティについてモデル検査を実施した結果新たに反例が得られた場合、その反例については、プログラムのミスかプロパティの不備かを改めて判定する。
【先行技術文献】
【特許文献】
【００３２】
【特許文献１】特開２００６−２３６０４２号公報
【特許文献２】特開２００８−２５０９１４号公報
【特許文献３】特開２００３−６２５５号公報
【発明の概要】
【発明が解決しようとする課題】
【００３３】
しかしながら、上述した従来手法では、生成可能な条件式の種類の数は、条件の雛形の数と関数の雛形の数に依存し、実際には膨大な種類の雛形が必要になり、雛形作成の負担が増大する。また、条件の雛形におけるパラメータに関数を再帰的に組み合わせる場合、その組み合わせ総数が膨大になる。また、関数の再帰関係等も考慮した引数の組み合わせ方も膨大である。
【００３４】
図４１は、従来手法における述語テンプレート、関数テンプレートの組み合わせを示す説明図である。図４１において、追加可能な述語の種類は、変数・パラメータの型を区別しない場合、述語テンプレート総数および述語テンプレートのパラメータ数の平均、関数テンプレートの総数および関数テンプレートのパラメータ数の平均、ならびにパラメータとして使用されるプログラム状態中の変数の数の積に比例する。また、関数が再帰的に呼ばれる場合を考えるとそれ以上となる。したがって、実際に追加すべき述語を全種類試すためには膨大な作業量・記録領域が必要になるという問題がある。
【００３５】
本開示技術は、上述した従来技術による問題点を解消するため、膨大な作業量・記憶領域を必要とすることなく、プロパティを適正に修正することができるプロパティ修正プログラム、プロパティ修正装置、およびプロパティ修正方法を提供することを目的とする。
【課題を解決するための手段】
【００３６】
上述した課題を解決し、目的を達成するため、本開示技術は、検査対象プログラムの設計上の性質・仕様を、該検査対象プログラムにおいて駆動されるイベントごとに、論理式で定義される事前条件と事後条件によって記述したプロパティについて、該プロパティの記述の誤りを修正するために、前記検査対象プログラムの実行によって、事前条件が真で事後条件が偽となったイベントに係るプロパティを、修正対象プロパティとして取得し、前記検査対象プログラムの初期状態から前記修正対象プロパティに係るイベントに到るまでに駆動された全イベントを特定する情報を含む状態遷移列を反例として検出するとともに、該検査対象プログラムの実行によって駆動された該修正対象プロパティに係るイベントと同一のイベントのうち、事前条件と事後条件とが共に真となったイベントを特定し、該初期状態から該特定されたイベントに到るまでに駆動された全イベントを特定する情報を含む状態遷移列を該反例に対する正例として検出し、検出された前記反例および前記正例の差分のイベントを特定する情報を含む差分状態遷移列を抽出し、抽出された前記差分状態遷移列に含まれるイベントに係るプロパティの前記事前条件および前記事後条件を論理積標準形に変換し、変換後の該事前条件および該事後条件に含まれる各節の論理式を、差分論理式として抽出し、抽出された前記差分論理式の真偽判定を、前記正例の最終のイベントの駆動元の状態と、前記反例の最終のイベントの駆動元の状態それぞれに基づいて行い、真偽判定結果が前記正例の最終のイベントの駆動元の状態と前記反例の最終のイベントの駆動元の状態とで異なる場合に、該差分論理式を候補論理式として生成し、生成された候補論理式を前記修正対象プロパティの事前条件に追加することにより、修正済プロパティを生成し、修正された修正済プロパティを出力することを要件とする。
【発明の効果】
【００３７】
本プロパティ修正プログラム、プロパティ修正装置、およびプロパティ修正方法によれば、膨大な作業量・記憶領域を必要とすることなく、プロパティを適正に修正することができるという効果を奏する。
【図面の簡単な説明】
【００３８】
【図１】本開示技術にかかる反例解析の概念を示す説明図である。
【図２】実施の形態１にかかるプロパティ修正装置のハードウェア構成を示すブロック図である。
【図３】解析対象の具体例を示す説明図である。
【図４】プロパティテーブルの記憶内容を示す説明図である。
【図５−１】プログラム状態テーブルの記憶状態（その１）を示す説明図である。
【図５−２】プログラム状態テーブルの記憶状態（その２）を示す説明図である。
【図５−３】プログラム状態テーブルの記憶状態（その３）を示す説明図である。
【図５−４】プログラム状態テーブルの記憶状態（その４）を示す説明図である。
【図５−５】プログラム状態テーブルの記憶状態（その５）を示す説明図である。
【図５−６】プログラム状態テーブルの記憶状態（その６）を示す説明図である。
【図５−７】プログラム状態テーブルの記憶状態（その７）を示す説明図である。
【図５−８】プログラム状態テーブルの記憶状態（その８）を示す説明図である。
【図５−９】プログラム状態テーブルの記憶状態（その９）を示す説明図である。
【図５−１０】プログラム状態テーブルの記憶状態（その１０）を示す説明図である。
【図５−１１】プログラム状態テーブルの記憶状態（その１１）を示す説明図である。
【図５−１２】プログラム状態テーブルの記憶状態（その１２）を示す説明図である。
【図５−１３】プログラム状態テーブルの記憶状態（その１３）を示す説明図である。
【図５−１４】プログラム状態テーブルの記憶状態（その１４）を示す説明図である。
【図５−１５】プログラム状態テーブルの記憶状態（その１５）を示す説明図である。
【図５−１６】プログラム状態テーブルの記憶状態（その１６）を示す説明図である。
【図５−１７】プログラム状態テーブルの記憶状態（その１７）を示す説明図である。
【図５−１８】プログラム状態テーブルの記憶状態（その１８）を示す説明図である。
【図５−１９】プログラム状態テーブルの記憶状態（その１９）を示す説明図である。
【図５−２０】プログラム状態テーブルの記憶状態（その２０）を示す説明図である。
【図５−２１】プログラム状態テーブルの記憶状態（その２１）を示す説明図である。
【図６】プログラム状態遷移テーブルの記憶状態を示す説明図である。
【図７】状態遷移列の一例を示す説明図である。
【図８】違反プロパティテーブルの記憶内容を示す説明図である。
【図９】差分論理式テーブルの記憶内容を示す説明図である。
【図１０】候補論理式テーブルの記憶内容を示す説明図である。
【図１１】プロパティ修正装置の機能的構成を示すブロック図である。
【図１２】検査部によるモデル検査例を示す説明図である。
【図１３】実施の形態１にかかる検出部による正例検出例を示す説明図である。
【図１４】実施の形態１にかかる反例側差分と正例側差分との抽出例を示す説明図である。
【図１５−１】論理式と論理式の否定との一例を示す説明図である。
【図１５−２】節と部分節との一例を示す説明図である。
【図１５−３】論理積標準形の一例を示す説明図である。
【図１６】差分論理式の抽出例を示す説明図である。
【図１７】実施の形態１にかかる候補論理式の生成例を示す説明図である。
【図１８】実施の形態１にかかる修正対象プロパティの修正例を示す説明図である。
【図１９】実施の形態１にかかるプロパティ修正装置によるプロパティ修正処理手順を示すフローチャートである。
【図２０】図１９に示したモデル検査処理（ステップＳ１９０１）の詳細な処理手順を示すフローチャートである。
【図２１】図１９に示した正例検出処理（ステップＳ１９０４）の詳細な処理手順を示すフローチャートである。
【図２２】図２１に示した反例中の正例チェック処理（ステップＳ２１０１）の詳細な処理手順を示すフローチャートである。
【図２３】図１９に示した差分論理式抽出処理（ステップＳ１９０７）の詳細な処理手順を示すフローチャートである。
【図２４】論理式集合とそのべき集合を示す説明図である。
【図２５】図１９に示した候補論理式生成処理（ステップＳ１９０９）の詳細な処理手順を示すフローチャートである。
【図２６】図１９に示した候補論理式追加によるプロパティ修正処理（ステップＳ１９１１）の詳細な処理手順を示すフローチャートである。
【図２７−１】反例テーブルの記憶内容を示す説明図である。
【図２７−２】正例テーブルの記憶内容を示す説明図である。
【図２８】比較済み正例テーブルの記憶内容を示す説明図である。
【図２９】実施の形態２にかかる検出部による反例・正例検出例を示す説明図である。
【図３０】実施の形態２にかかる反例側差分と正例側差分との抽出例を示す説明図である。
【図３１】実施の形態２にかかる候補論理式の生成例を示す説明図である。
【図３２−１】実施の形態２にかかる修正対象プロパティの修正例（その１）を示す説明図である。
【図３２−２】実施の形態２にかかる修正対象プロパティの修正例（その２）を示す説明図である。
【図３２−３】実施の形態２にかかる修正対象プロパティの修正例（その３）を示す説明図である。
【図３２−４】実施の形態２にかかる修正対象プロパティの修正例（その４）を示す説明図である。
【図３２−５】実施の形態２にかかる修正対象プロパティの修正例（その５）を示す説明図である。
【図３２−６】実施の形態２にかかる修正対象プロパティの修正例（その６）を示す説明図である。
【図３３】図３２−６で得られた修正済プロパティの事前条件の真偽を示す説明図である。
【図３４】実施の形態２にかかるプロパティ修正装置によるプロパティ修正処理手順を示すフローチャート（その１）である。
【図３５】実施の形態２にかかるプロパティ修正装置によるプロパティ修正処理手順を示すフローチャート（その２）である。
【図３６】図３４に示した全反例検出処理（ステップＳ３４０４）の詳細な処理手順を示すフローチャートである。
【図３７】図３４に示した全正例検出処理（ステップＳ３４０５）の詳細な処理手順を示すフローチャートである。
【図３８】図３５に示した候補論理式生成処理（ステップＳ３５１０）の詳細な処理手順を示すフローチャートである。
【図３９】事前条件不足解消前後を示す説明図である。
【図４０】従来手法を示す説明図である。
【図４１】従来手法における述語テンプレート、関数テンプレートの組み合わせを示す説明図である。
【発明を実施するための形態】
【００３９】
以下に添付図面を参照して、本開示技術にかかるプロパティ修正プログラム、プロパティ修正装置、およびプロパティ修正方法の好適な実施の形態を詳細に説明する。
【００４０】
図１は、本開示技術にかかる反例解析の概念を示す説明図である。本開示技術では、反例に加え、正例とそれに対応するプロパティを利用する。具体的には、反例と正例の差分をとる。また、正例側あるいは反例側の差分状態遷移列で用いられているプロパティ中の条件を、不足条件の候補として利用する。
【００４１】
＜実施の形態１＞
まず、本開示技術にかかる反例解析の概念を利用した反例解析について説明する。ここでは、具体例を挙げて説明する。本開示技術の反例解析ソフトウェアは、以下に示すハードウェア構成を持つコンピュータにインストールされて実行される。
【００４２】
（反例解析装置のハードウェア構成）
図２は、実施の形態１にかかるプロパティ修正装置のハードウェア構成を示すブロック図である。図２において、プロパティ修正装置は、ＣＰＵ（Ｃｅｎｔｒａｌ  Ｐｒｏｃｅｓｓｉｎｇ  Ｕｎｉｔ）２０１と、ＲＯＭ（Ｒｅａｄ‐Ｏｎｌｙ  Ｍｅｍｏｒｙ）２０２と、ＲＡＭ（Ｒａｎｄｏｍ  Ａｃｃｅｓｓ  Ｍｅｍｏｒｙ）２０３と、磁気ディスクドライブ２０４と、磁気ディスク２０５と、光ディスクドライブ２０６と、光ディスク２０７と、ディスプレイ２０８と、Ｉ／Ｆ（Ｉｎｔｅｒｆａｃｅ）２０９と、キーボード２１０と、マウス２１１と、スキャナ２１２と、プリンタ２１３と、を備えている。また、各構成部はバス２００によってそれぞれ接続されている。
【００４３】
ここで、ＣＰＵ２０１は、プロパティ修正装置の全体の制御を司る。ＲＯＭ２０２は、ブートプログラムなどのプログラムを記憶している。ＲＡＭ２０３は、ＣＰＵ２０１のワークエリアとして使用される。磁気ディスクドライブ２０４は、ＣＰＵ２０１の制御にしたがって磁気ディスク２０５に対するデータのリード／ライトを制御する。磁気ディスク２０５は、磁気ディスクドライブ２０４の制御で書き込まれたデータを記憶する。
【００４４】
光ディスクドライブ２０６は、ＣＰＵ２０１の制御にしたがって光ディスク２０７に対するデータのリード／ライトを制御する。光ディスク２０７は、光ディスクドライブ２０６の制御で書き込まれたデータを記憶したり、光ディスク２０７に記憶されたデータをコンピュータに読み取らせたりする。
【００４５】
ディスプレイ２０８は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイ２０８は、たとえば、ＣＲＴ、ＴＦＴ液晶ディスプレイ、プラズマディスプレイなどを採用することができる。
【００４６】
インターフェース（以下、「Ｉ／Ｆ」と略する。）２０９は、通信回線を通じてＬＡＮ（Ｌｏｃａｌ  Ａｒｅａ  Ｎｅｔｗｏｒｋ）、ＷＡＮ（Ｗｉｄｅ  Ａｒｅａ  Ｎｅｔｗｏｒｋ）、インターネットなどのネットワーク２１４に接続され、このネットワーク２１４を介して他の装置に接続される。そして、Ｉ／Ｆ２０９は、ネットワーク２１４と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。Ｉ／Ｆ２０９には、たとえばモデムやＬＡＮアダプタなどを採用することができる。
【００４７】
キーボード２１０は、文字、数字、各種指示などの入力のためのキーを備え、データの入力をおこなう。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウス２１１は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などをおこなう。ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。
【００４８】
スキャナ２１２は、画像を光学的に読み取り、プロパティ修正装置内に画像データを取り込む。なお、スキャナ２１２は、ＯＣＲ（Ｏｐｔｉｃａｌ  Ｃｈａｒａｃｔｅｒ  Ｒｅａｄｅｒ）機能を持たせてもよい。また、プリンタ２１３は、画像データや文書データを印刷する。プリンタ２１３には、たとえば、レーザプリンタやインクジェットプリンタを採用することができる。
【００４９】
（解析対象の具体例）
図３は、解析対象の具体例を示す説明図である。図３では、一例として電子商取引サイト用のＷｅｂアプリケーションプログラムを用いる。Ｗｅｂアプリケーションプログラムはログイン画面３０１、メニュー画面３０２、支払い確認画面３０５、商品選択画面３０３、アンケート画面３０４という５つの利用者向け画面を持ち、６つのイベントＥ１〜Ｅ６によって駆動して画面遷移、データ更新等の処理を行う。ここで、イベントＥ１はログイン実行、イベントＥ２は商品一覧選択、イベントＥ３はトップメニューへ戻る、イベントＥ４はアンケート選択、イベントＥ５はアンケート回答、イベントＥ６は支払い内容確認選択という内容のイベントである。
【００５０】
ログイン画面３０１には会員ＩＤおよびパスワードを入力する各テキストボックスおよびログインボタンがある。会員ＩＤおよびパスワードを入力し、ログインボタンを押下することで、イベントＥ１が駆動され、メニュー画面３０２に遷移する。図３では、会員ＩＤ入力用のテキストボックスに「ｓｏｆｔ」、パスワード入力用のテキストボックスには入力文字をマスクした「＊＊＊＊＊＊＊」が入力されている。
【００５１】
メニュー画面３０２では、ログイン者の会員ＩＤを含むウェルカムメッセージ、ログイン者の会員ＩＤに紐づいた電子商取引サービスの決済回数である利用回数、決済を含むコンテンツを利用することで累積するポイントおよび会員種別が表示されている。また、商品一覧、アンケート、ログアウトのボタンがある。ここでは、ログアウトに紐づいたイベントは実行されないとする。
【００５２】
また、アンケートボタンの右側にはアンケートに回答したかどうかを示すメッセージが表示される。メニュー画面３０２において商品一覧ボタンを押下することでイベントＥ２が駆動されて商品選択画面３０３へ遷移する。また、アンケートボタンを押下することでイベントＥ４が駆動されてアンケート画面３０４へ遷移する。図３では、画面左上に「ようこそｓｏｆｔさん」というウェルカムメッセージが、ウェルカムメッセージの右側にログイン者の会員種別「正会員」が表示されている。
【００５３】
また、それらメッセージの下部にログイン者の利用回数「２５」が、さらにその下部にログイン者の累計ポイント「４５００」が表示されている。また、アンケートボタンの右側にはログイン者がまだアンケートに回答していないことを示す「未回答」が表示されている。
【００５４】
商品選択画面３０３では、ログイン者の会員ＩＤを含む商品一覧メッセージ、ログイン者の会員ＩＤに紐づいた会員種別、ログイン者向けの特別商品があれば特別商品一覧、通常商品一覧が表示されている。
【００５５】
また、トップメニュー、支払い内容確認のボタンがある。表示される特別商品一覧および通常商品一覧は商品名、価格、数量の３カラムからなるテーブルである。数量は利用者が対応する商品の希望購入数量を入力するためのテキストボックスとなっている。商品選択画面３０３においてトップメニューボタンを押すことでイベントＥ３が駆動されてメニュー画面３０２へ遷移する。
【００５６】
また、支払い内容確認ボタンを押すことでイベントＥ６が駆動されて支払い確認画面へ遷移する。図３では、画面左上に「ｓｏｆｔさん向け商品一覧」という商品一覧メッセージが、商品一覧メッセージの右側にログイン者の会員種別「正会員」が表示されている。また、それらメッセージの下部に特別商品一覧が表示されている。また、特別商品一覧は、商品名「松坂牛ロース５００ｇ」、価格「６０００」、数量「０」というレコードと、商品名「ふぐさし」、価格「７５００」、数量「１」というレコードからなるテーブルである。
【００５７】
特別商品一覧の下部には通常商品一覧が表示されている。通常商品一覧は、商品名「コーヒー豆」、価格「５５０」、数量「１」というレコードと、商品名「レトルトカレー（辛口）」、価格「２５０」、数量「２」というレコードと、商品名「レトルトカレー（中辛）」、価格「２５０」、数量「０」というレコードからなるテーブルである。
【００５８】
アンケート画面３０４では、ログイン者のアンケート回答状況、アンケートに回答した場合の特典、質問・質問の回答欄が表示されている。アンケート画面３０４には回答ボタンがある。アンケート画面３０４で回答ボタンを押下することでイベントＥ５が駆動されて特典がログイン者に与えられ、メニュー画面３０２へ遷移する。ここでは、アンケートに回答した場合の特典はログイン者のポイントに１０００ポイントを加算するものとする。
【００５９】
図３では、ログイン者のアンケート回答状況「未回答」が画面右上に表示され、その下部にアンケートに回答した場合の特典「お答えいただくと１０００ポイントプレゼント」が表示されている。特典の下部に質問・質問の回答欄が続くが、図３では省略している。
【００６０】
支払い確認画面３０５では、ログイン者の会員ＩＤを含む支払い内容確認メッセージ、ログイン者の会員種別、ログイン者が特別割引対象者ならば特別割引価格であることを示す割引対象メッセージ、商品の購入点数、合計金額、割引金額、支払い金額、これまでの累計ポイント、今回の支払いによる新規獲得ポイント、支払い後の積算ポイントが表示される。
【００６１】
また、支払い確認画面には中止ボタンと購入ボタンがある。中止ボタンと購入ボタンを押下した際のイベントはここでは考えない。図３では、画面上部に支払い内容確認メッセージ「ｓｏｆｔさんのお支払い内容確認」、支払い内容確認メッセージの右側に会員種別、それらメッセージの下部に割引対象メッセージ「ｓｏｆｔさんには特別割引価格でご案内します！」が表示されている。
【００６２】
また、割引対象メッセージの左下部に、購入点数「４」、合計金額「８５００」、割引金額「８５０」、支払い金額「７６５０」が表示されている。また、割引対象メッセージの右下部に、累計ポイント「５５００」、新規獲得ポイント「７６」、支払い後の積算ポイント「５５７６」が表示されている。
【００６３】
Ｗｅｂアプリケーションはセッションを管理し、画面を構成するためのセッション管理情報として、画面名、会員ＩＤ、パスワード、会員種別、アンケート回答状況、購入時のサービスといった情報を用いている。モデル検査時には利用者に表示する画面情報でなく、前記セッション管理情報を格納する変数「画面．画面名」、「画面．会員ＩＤ」、「画面．パスワード」、「画面．会員種別」、「画面．アンケート」、「画面．サービス」の状態をプログラム状態として利用する。
【００６４】
ただし、利用者に表示する画面情報のうち、商品選択画面３０３で表示する特別商品一覧テーブルの長さ「長さ（画面．特別商品一覧）」の状態はプログラム状態に含める。ただし、プログラム状態は本例に限定されない。なお、Ｗｅｂアプリケーションは会員ＩＤに紐づく会員情報（会員種別、累計ポイント、利用回数）をデータベースで管理しており、会員Ｘの会員情報を「会員情報（会員種別，Ｘ）」、「会員情報（累計ポイント，Ｘ）」、「会員情報（利用回数，Ｘ）」で参照するものとする。これらデータベースの状態もモデル検査時のプログラム状態に含める。
【００６５】
（各種テーブルの記憶内容）
つぎに、実施の形態１で用いる各種テーブルの記憶内容について説明する。実施の形態１では、プロパティテーブル、プログラム状態テーブル、プログラム状態遷移テーブル、違反プロパティテーブル、差分論理式テーブル、候補論理式テーブルを用いる。これらテーブルは、具体的には、たとえば、図２に示したＲＯＭ２０２、ＲＡＭ２０３、磁気ディスク２０５、光ディスク２０７などの記憶装置に記憶される。以下、順に説明する。
【００６６】
図４は、プロパティテーブルの記憶内容を示す説明図である。プロパティテーブル４００とは、プロパティごとにプロパティの内容を記憶するテーブルである。具体的には、プロパティ名、評価イベント、事前条件、事後条件をフィールド項目とし、プロパティごとにレコードを有する。ここで、評価イベントとは、プロパティに評価されるイベントである。
【００６７】
プロパティテーブル４００において、たとえば、２行目のレコードで示されるプロパティＰ＿Ｅ１＿２は、ログイン画面３０１で会員種別が“ｎｏｒｍａｌ”と判断される（事前条件）と、遷移後の画面において、“正会員”と表示される（事後条件）ことを示している。
【００６８】
図５−１〜図５−２１は、プログラム状態テーブルの記憶状態を示す説明図である。プログラム状態テーブル５００とは、モデル検査実行時に遷移したプログラム状態を記録するテーブルである。具体的には、プログラム状態、変数名、変数値をフィールド項目とし、プログラム状態ごとにレコードを有する。
【００６９】
ここで、プログラム状態とは、レコードが言及しているプログラム状態の識別子である。また、変数名とは、対応するプログラム状態において値を記録している変数の識別子である。また、変数値とは、対応するプログラム状態において変数名で参照される変数が持つ値である。なお、網掛けのレコードは、網掛けではないレコードとログインしているユーザが異なることを示している。
【００７０】
図６は、プログラム状態遷移テーブルの記憶状態を示す説明図である。プログラム状態遷移テーブル６００とは、モデル検査実行時、イベントの駆動によって、プログラム状態がどのように遷移したかを記録するテーブルである。状態遷移図と等価である。具体的には、状態遷移名、イベント前状態、駆動イベント、イベント後状態をフィールド項目とし、状態遷移ごとにレコードを有する。
【００７１】
ここで、状態遷移名とは、状態遷移を一意に識別するための識別子である。イベント前状態とは、イベント駆動直前のプログラム状態の識別子である。駆動イベントとは、イベント前状態において駆動するイベント名である。イベント後状態とは、駆動イベントに記述されているイベント駆動直後のプログラム状態の識別子である。
【００７２】
なお、本明細書において、正例・反例・差分状態遷移列等のプログラム状態遷移列は、「状態（イベント）→状態（イベント）→．．．→状態（イベント）→状態」と表現する。
【００７３】
図７は、状態遷移列の一例を示す説明図である。図７に示した状態遷移列は、以下のように表現される。
Ｓ１（Ｅ１）→Ｓ２（Ｅ４）→Ｓ３（Ｅ５）→Ｓ４（Ｅ２）→Ｓ５（Ｅ６）→Ｓ６
【００７４】
図８は、違反プロパティテーブル８００の記憶内容を示す説明図である。違反プロパティテーブル８００とは、モデル検査でプロパティ違反が発生した場合に、違反したプロパティのプロパティ名を記録するテーブルである。
【００７５】
図９は、差分論理式テーブルの記憶内容を示す説明図である。差分論理式テーブル９００とは、差分ごとに、それぞれ１つの正例と反例に関する差分論理式を保持するテーブルである。具体的には、差分名、差分内容をフィールド項目とし、差分ごとにレコードを有する。ここで、差分名とは、差分論理式テーブル９００内において、差分論理式を一意に特定する識別子である。差分内容とは、差分名に対応する差分を表現した論理式である。差分論理式テーブル９００の初期状態は空であり、後述する差分論理式抽出部により抽出される差分論理式が順次追加される。
【００７６】
図１０は、候補論理式テーブルの記憶内容を示す説明図である。候補論理式テーブル１０００とは、候補となる差分ごとに、それぞれ１つの正例と反例に関する候補論理式を保持するテーブルである。具体的には、差分名、ＮＯＴ付加フラグをフィールド項目とし、差分ごとにレコードを有する。
【００７７】
ここで、ＮＯＴ付加フラグとは、差分名が指す論理式を修正対象プロパティの事前条件にＡＮＤ結合する場合に、論理式の否定（ＮＯＴ）を結合するのか論理式そのものを結合するのかを判断するためのフラグである。「付加する」である場合、対応する論理式の否定を結合する。一方、「付加しない」である場合、対応する論理式そのものを結合する。候補論理式テーブル１０００の初期状態は空であり、後述する生成部により抽出される候補論理式となる差分名およびＮＯＴ付加フラグが順次追加される。
【００７８】
（反例解析装置の機能的構成）
図１１は、プロパティ修正装置の機能的構成を示すブロック図である。反例解析装置１１００は、検査部１１０１と、検出部１１０２と、差分抽出部１１０３と、差分論理式抽出部１１０４と、生成部１１０５と、修正部１１０６と、出力部１１０７と、を含む構成である。この制御部となる機能（検査部１１０１〜出力部１１０７）は、具体的には、たとえば、図２に示したＲＯＭ２０２、ＲＡＭ２０３、磁気ディスク２０５、光ディスク２０７などの記憶装置に記憶されたプログラムをＣＰＵ２０１に実行させることにより、または、Ｉ／Ｆ２０９により、その機能を実現する。
【００７９】
検査部１１０１は、検査対象プログラムを検査する機能を有する。検査部１１０１のモデル検査に先立って、検証者が、モデル検査実施に用いるプロパティテーブル４００（図４を参照。）を作成する。そして、反例解析装置１１００にプロパティテーブル４００を読み込ませておく。このあと、検査対象プログラムを走らせてモデル検査を実行すると、検査部１１０１は、プロパティ違反までのプログラム状態テーブル５００、プログラム状態遷移テーブル６００、違反プロパティテーブル８００を自動作成する。
【００８０】
図１２は、検査部１１０１によるモデル検査例を示す説明図である。図１２に示したプログラム状態遷移列では、ログイン画面３０１（プログラム状態Ｓ１）からイベントＥ１を駆動してメニュー画面３０２（プログラム状態Ｓ２）へ至る。つぎに、イベントＥ４を駆動してアンケート画面３０４（プログラム状態Ｓ３）へ至る。その後、イベントＥ５を駆動してメニュー画面３０２（プログラム状態Ｓ４）へ至る。さらに、イベントＥ２を駆動して商品選択画面３０３（プログラム状態Ｓ５）へ至る。その後、イベントＥ６を駆動して支払い確認画面３０５（プログラム状態Ｓ６）に至る。
【００８１】
プログラム状態遷移列のうち、プログラム状態Ｓ５における変数「画面.会員種別」の値が「正会員」であるのに、イベントＥ６駆動後のプログラム状態における変数「画面.サービス」の値が「割引サービス」になっている。
【００８２】
すなわち、図４に示したプロパティＰ＿Ｅ６＿２の事前条件が真でありながら事後条件が真でなく、上述した［評価２］の通りに評価されている。したがって、プログラム状態遷移列は、プロパティＰ＿Ｅ６＿２に違反している。同時に、プロパティ違反に至る状態遷移列“Ｓ１（Ｅ１）→Ｓ２（Ｅ４）→Ｓ３（Ｅ５）→Ｓ４（Ｅ２）→Ｓ５（Ｅ６）→Ｓ６”が反例となる。したがって、検査部１１０１を実行することにより、反例も同時に検出される。
【００８３】
なお、本例では、プロパティ違反に至る状態遷移列“Ｓ１（Ｅ１）→Ｓ２（Ｅ４）→Ｓ３（Ｅ５）→Ｓ４（Ｅ２）→Ｓ５（Ｅ６）→Ｓ６”に含まれない状態遷移は実施されておらず、プロパティＰ＿Ｅ６＿２以外のプロパティ違反は検出されていないものと仮定する。すなわち、プログラム状態テーブル５００にはプログラム状態Ｓ１〜Ｓ６が保持され、プログラム状態遷移テーブル６００にはＳ１（Ｅ１）→Ｓ２、Ｓ２（Ｅ４）→Ｓ３、Ｓ３（Ｅ５）→Ｓ４、Ｓ４（Ｅ２）→Ｓ５、Ｓ５（Ｅ６）→Ｓ６のみが記録されているものとする。
【００８４】
図１１において、検出部１１０２は、検査部１１０１によって検査されたモデル検査結果となる検査対象プログラムのプログラム状態遷移列から、正例を検出する機能を有する。
【００８５】
図１３は、実施の形態１にかかる検出部１１０２による正例検出例を示す説明図である。検出する正例は反例と比較して最もプログラム状態遷移列上での共通部分が多いもののうちの１つとなるようにする。そのような正例の選択基準を設けた理由は、当該反例と共通部分が多い正例の方がより当該反例とのプログラム状態遷移列上の差が小さく、小さい差の中で評価されたイベントに関するプロパティ中の条件が関係する傾向が強いと考えられるためである。むろん正例の選択基準を変更してもよい。
【００８６】
具体的には、反例の末尾のプログラム状態からバックトレースして分岐ノードとなるプログラム状態を検出する。そして、検出された分岐ノードからフォワードトレースして末尾のプログラム状態に到達し、かつ末尾のプログラム状態において反例の違反プロパティの事前条件および事後条件が真と評価される場合、検出された分岐ノードから到達した末尾のノードまでの状態遷移列を正例とする。
【００８７】
本例では、反例“Ｓ１（Ｅ１）→Ｓ２（Ｅ４）→Ｓ３（Ｅ５）→Ｓ４（Ｅ２）→Ｓ５（Ｅ６）→Ｓ６”に対して正例“Ｓ１（Ｅ１）→Ｓ２（Ｅ２）→Ｓ８（Ｅ６）→Ｓ９”が検出される。
【００８８】
正例を言い換えると、メニュー画面３０２（プログラム状態Ｓ２）からイベントＥ２を駆動して商品選択画面３０３（プログラム状態Ｓ８）に至り、さらにイベントＥ６を駆動して支払い確認画面３０５（プログラム状態Ｓ９）に至る状態遷移列である。プログラム状態Ｓ８で違反プロパティＰ＿Ｅ６＿２の事前条件が真（「画面．会員種別」＝正会員）になり、また、プログラム状態Ｓ９で違反プロパティＰ＿Ｅ６＿２の事後条件が真（「画面．サービス」＝サービスなし）になる。
【００８９】
また、正例検出までのプログラム状態の探索の結果、新たにプログラム状態Ｓ７〜Ｓ９がプログラム状態テーブル５００に追加される。また、プログラム状態遷移「Ｓ５（Ｅ３）→Ｓ４」、「Ｓ４（Ｅ４）→Ｓ７」、「Ｓ７（Ｅ５）→Ｓ４」、「Ｓ２（Ｅ２）→Ｓ８」、「Ｓ８（Ｅ３）→Ｓ２」、「Ｓ８（Ｅ６）→Ｓ９」がプログラム状態遷移テーブル６００に追加される。
【００９０】
図１１において、差分抽出部１１０３は、反例と正例との差分を抽出する機能を有する。具体的には、たとえば、正例を検出した際の分岐ノードから反例の末尾までのプログラム状態遷移列を反例側差分として抽出する。同様に、正例を検出した際の分岐ノードから正例の末尾までのプログラム状態遷移列を正例側差分として抽出する。
【００９１】
図１４は、実施の形態１にかかる反例側差分と正例側差分との抽出例を示す説明図である。実施の形態１では、正例側差分を差分状態遷移列として利用する。反例側差分は利用しない。
【００９２】
図１１において、差分論理式抽出部１１０４は、正例側差分である差分状態遷移列において駆動するイベントに関するプロパティの事前・事後条件から、違反プロパティの事前条件にＡＮＤ追加すべき差分論理式を抽出する機能を有する。具体的には、差分状態遷移列中で駆動されるイベントに関するプロパティから事前条件と事後条件を取り出す。つぎに、それぞれの論理積標準形を計算する。
【００９３】
論理積標準形とは、複数の節をＡＮＤ結合した論理式である。節とは、複数の原子論理式をそれぞれＯＲ結合した論理式である。原子論理式とは、論理式の最小単位（単独の条件）またはその否定である。論理式とは、上述したように、プロパティに記述する条件（事前条件または事後条件）をあらわす式である。論理式の否定とは、論理式にＮＯＴを結合した論理式である。
【００９４】
図１５−１は、論理式と論理式の否定との一例を示す説明図である。ＮＯＴを結合した論理式が真の場合、その否定は偽であり、ＮＯＴを結合した論理式が偽の場合、その否定は真である。
【００９５】
図１５−２は、節と部分節との一例を示す説明図である。複数の原子論理式をそれぞれＯＲ結合した原子論理式（節）のいずれかが真の場合、その節は真である。また、複数の原子論理式をそれぞれＯＲ結合した原子論理式（節）のすべてが偽の場合、その節は偽である。原子論理式自体も節の一種である。節自体も論理積標準形の一種である。また、部分節とは、節に用いられている原子論理式のいくつかをＯＲ結合した論理式である。部分節も節の一種である。
【００９６】
図１５−３は、論理積標準形の一例を示す説明図である。複数の節をＡＮＤ結合した節のすべてが真の場合、その論理積標準形は真である。複数の節をＡＮＤ結合した節のいずれかが偽の場合、その論理積標準形は偽である。節自体も論理積標準形の一種である。すべての論理式は論理積標準形に変換可能である。
【００９７】
図１１において、差分論理式抽出部１１０４は、計算した論理積標準形に存在する各節をまず差分論理式の１つとし、さらに当該各節の部分節も差分論理式の１つとする。節を選ぶ理由は、修正対象プロパティの事前条件に条件を追加する際に、事前条件が少なくとも弱くならないように必ずＡＮＤで追加するのだが、その際もＯＲを含む条件が追加できるようにするためである。
【００９８】
図１６は、差分論理式の抽出例を示す説明図である。まず、プロパティテーブル４００から、評価イベントが、差分状態遷移列“Ｓ２（Ｅ２）→Ｓ８（Ｅ６）→Ｓ９”中で駆動されるイベントＥ２，Ｅ６となるプロパティＰ＿Ｅ２＿１，Ｐ＿Ｅ２＿２，Ｐ＿Ｅ６＿１を抽出する。修正対象プロパティＰ＿Ｅ６＿２も該当するが、修正対象であるため抽出対象外である。
【００９９】
プロパティＰ＿Ｅ２＿１の事前条件は、ただ１つの節
「（画面．会員種別＝＝“プレミアム”）ＯＲ（会員情報（累計ポイント，画面．会員ＩＤ）＞＝５０００）」
となる。
【０１００】
この節は、すでに論理積標準形であるので、節自身（ここでは事前条件自身）および各部分節「（画面．会員種別＝＝“プレミアム”）」，「（会員情報（累計ポイント，画面．会員ＩＤ）＞＝５０００）」が差分論理式（差分１〜差分３）として差分論理式テーブル９００に追加する。
【０１０１】
プロパティＰ＿Ｅ２＿１の事後条件は、原子論理式「（長さ（画面．特別商品一覧）＞＝１）」であるので、事後条件自身のみを差分論理式（差分６）として差分論理式テーブル９００に追加する。
【０１０２】
プロパティＰ＿Ｅ２＿２の事前条件は「（画面．会員種別＝＝“正会員”）ＡＮＤ（会員情報（累計ポイント，画面．会員ＩＤ）＜３０００）」と２つの節（原子論理式）からなる論理積標準形である。したがって、各節に相当する原子論理式「（画面．会員種別＝＝“正会員”）」，「（会員情報（累計ポイント，画面．会員ＩＤ）＜３０００）」を差分論理式（差分４，差分５）として差分論理式テーブル９００に追加する。
【０１０３】
プロパティＰ＿Ｅ２＿２の事後条件「（長さ（画面．特別商品一覧）＝＝０）」，プロパティＰ＿Ｅ６＿１の事前条件「（画面．会員種別＝＝“プレミアム”）」，プロパティＰ＿Ｅ６＿１の事後条件「（画面．サービス＝＝“割引サービス”）」はプロパティＰ＿Ｅ２＿１の事後条件と同様に原子論理式である。したがって、すでに差分２として同じものが追加されている前記Ｐ＿Ｅ６＿１の事前条件を除いた各条件自身を差分論理式（差分７，差分８）として差分論理式テーブル９００に追加する。
【０１０４】
図１１において、生成部１１０５は、差分論理式と正例・反例および正例・反例中のプログラム状態から候補論理式を生成する機能を有する。生成された候補論理式は、候補論理式に登録される。候補論理式から１つ選択して、反例のプログラム状態遷移列の事前条件に追加することで反例をガードする。
【０１０５】
具体的には、正例・反例中で最後に駆動されたイベントである修正対象プロパティ評価イベント駆動直前のプログラム状態をそれぞれ取得する。図１３に示したプログラム状態遷移列を例に挙げると、正例で最後に駆動されたイベントＥ６の直前のプログラム状態Ｓ８と反例で最後に駆動されたイベントＥ６の直前のプログラム状態Ｓ５を取得する。そして、差分論理式テーブル９００の評価（真偽判定）を、取得した各プログラム状態Ｓ５，Ｓ８に対して実行する。
【０１０６】
図１７は、実施の形態１にかかる候補論理式の生成例を示す説明図である。正例側のプログラム状態Ｓ８については、図５−１０に示したプログラム状態テーブル５００を用いる。同様に、反例側のプログラム状態Ｓ５については、図５−７に示したプログラム状態テーブル５００を用いる。
【０１０７】
たとえば、プログラム状態Ｓ８に着目すると、差分１は、図５−１０に示したプログラム状態テーブル５００のどのレコードも満たさないため、評価結果は「偽」となる。また、差分４は、図５−１０に示したプログラム状態テーブル５００の｛変数名：画面．会員種別、変数：正会員｝と一致するため、評価結果は「真」となる。プログラム状態Ｓ５についても図５−７に示したプログラム状態テーブル５００を用いて同様に評価する。
【０１０８】
そして、両評価結果を比較して、評価が異なる差分論理式を候補となる差分論理式（候補論理式）に決定する。そして、決定された候補論理式の差分名を候補論理式テーブル１０００に追加する。図１７では、差分１、差分３、差分６、差分７が追加される。
【０１０９】
この場合、正例側の評価結果が偽である候補論理式に対しては、候補論理式テーブル１０００中のＮＯＴ付加フラグを「付加する」に設定する。また、正例側の評価結果が真である候補論理式に対しては、候補論理式テーブル１０００中のＮＯＴ付加フラグを「付加しない」に設定する。ＮＯＴ付加フラグをこのように設定する理由は、候補論理式を修正対象プロパティの事前条件に付加する際に、正例側のプログラム状態で評価結果が真となるように付加しなければ正例が維持されず、反例もガードされないためである。
【０１１０】
図１１において、修正部１１０６は、候補論理式および修正対象プロパティから、修正済プロパティを生成する機能を有する。具体的には、候補論理式テーブル１０００から少なくとも１つの任意の候補論理式を選択する。そして、選択した候補論理式に関連付けられているＮＯＴ付加フラグが「付加する」であれば、候補論理式の否定を修正対象プロパティにＡＮＤ追加する。一方、選択した候補論理式に関連付けられているＮＯＴ付加フラグが「付加しない」であれば、候補論理式自身を修正対象プロパティの事前条件にＡＮＤ追加する。
【０１１１】
ＮＯＴ付加フラグに従って修正対象プロパティの事前条件にＡＮＤ追加される候補論理式または候補論理式の否定は、検出した正例中の最後のイベントである修正対象プロパティが評価されるイベント駆動直前のプログラム状態で真と評価される。一方、検出した反例中の最後のイベントである修正対象プロパティが真と評価されるイベント駆動直前のプログラム状態で偽と評価される。
【０１１２】
したがって、候補論理式または候補論理式の否定を修正対象プロパティの事前条件にＡＮＤ追加した条件は、正例側のプログラム状態で成立し、反例側のプログラム状態で成立しない。これにより、反例のガードと正例の維持という事前条件不足解消の要件を満たす。
【０１１３】
図１８は、実施の形態１にかかる修正対象プロパティの修正例を示す説明図である。修正部１１０６では、候補論理式テーブル１０００の中で、差分１の候補論理式を選択する。選択された差分１のＮＯＴ付加フラグの値「付加する」に従って、差分１の否定「ＮＯＴ（会員情報（累計ポイント，画面．会員ＩＤ）＞＝５０００）」を修正対象プロパティの事前条件にＡＮＤ追加する。
【０１１４】
そして、ＡＮＤ追加されたプロパティ「駆動イベント：Ｅ６、事前条件：（画面．会員種別＝＝“正会員”）ＡＮＤ  ＮＯＴ（会員情報（累計ポイント，画面．会員ＩＤ）＞＝５０００）、事後条件：（画面．サービス＝＝“サービスなし”）」を修正済プロパティとして格納する。
【０１１５】
なお、プロパティ修正を実行するために必要な正例、差分論理式、候補論理式のいずれかが存在していない場合、反例解析装置によるプロパティ修正は失敗となり、ユーザは、手動でプロパティを修正することとなる。なお、候補論理式または差分論理式が存在しない場合には、別の正例の検出を試みてもよい。
【０１１６】
図１１において、出力部１１０７は、修正が成功した場合の修正結果（修正済プロパティ）、修正する必要がない旨の通知、修正失敗を出力する機能を有する。具体的には、たとえば、ディスプレイに表示したり、他の装置に送信したり、プリンタに印刷出力する。また、記憶装置内の記憶領域に格納することとしてもよい。
【０１１７】
（反例解析処理手順）
図１９は、実施の形態１にかかるプロパティ修正装置による反例解析処理手順を示すフローチャートである。まず、検査部１１０１によりモデル検査処理を実行する（ステップＳ１９０１）。モデル検査処理（ステップＳ１９０１）については、図２０で詳細に説明する。
【０１１８】
つぎに、モデル検査処理の検査結果に違反プロパティがあるか否かを判断する（ステップＳ１９０２）。違反プロパティがない場合（ステップＳ１９０２：Ｎｏ）、プロパティを修正する必要がないため、ステップＳ１９１２に移行する。
【０１１９】
一方、違反プロパティがある場合（ステップＳ１９０２：Ｙｅｓ）、違反プロパティを修正対象プロパティとして１つ選択する（ステップＳ１９０３）。そして、検出部１１０２により正例検出処理を実行する（ステップＳ１９０４）。正例検出処理（ステップＳ１９０４）については、図２１で後述する。
【０１２０】
そして、正例検出処理（ステップＳ１９０４）で正例が検出されたか否かを判断する（ステップＳ１９０５）。正例が検出された場合（ステップＳ１９０５：Ｙｅｓ）、差分抽出部１１０３により、修正対象プロパティにおける正例と反例との差分を抽出する（ステップＳ１９０６）。このあと、差分論理式抽出部１１０４により、差分論理式抽出処理を実行する（ステップＳ１９０７）。そして、差分論理式があるか否かを判断する（ステップＳ１９０８）。差分論理式がある場合（ステップＳ１９０８：Ｙｅｓ）、生成部１１０５により候補論理式生成処理を実行する（ステップＳ１９０９）。
【０１２１】
そして、候補論理式があるか否かを判断する（ステップＳ１９１０）。候補論理式がある場合（ステップＳ１９１０：Ｙｅｓ）、修正部１１０６により、候補論理式追加によるプロパティ修正処理を実行する（ステップＳ１９１１）。このあと、出力部１１０７により結果出力（修正済プロパティや修正不要通知）をおこない（ステップＳ１９１２）、一連の処理を終了する。
【０１２２】
一方、ステップＳ１９０５において正例が検出されなかった場合（ステップＳ１９０５：Ｎｏ）、出力部１１０７によりＮＧ（Ｎｏ  Ｇｏｏｄ）出力（修正失敗）をおこなう（ステップＳ１９１３）。また、ステップＳ１９０８において差分論理式がない場合（ステップＳ１９０８：Ｎｏ）、出力部１１０７によりＮＧ出力（修正失敗）をおこなう（ステップＳ１９１３）。同様に、ステップＳ１９１０において候補論理式がない場合（ステップＳ１９１０：Ｎｏ）、出力部１１０７によりＮＧ出力（修正失敗）をおこなう（ステップＳ１９１３）。そして、一連の処理を終了する。
【０１２３】
図２０は、図１９に示したモデル検査処理（ステップＳ１９０１）の詳細な処理手順を示すフローチャートである。モデル検査処理では、あらかじめ検査対象プログラムとプロパティテーブル４００を与えておく。モデル検査処理は、検証対象プログラムがプロパティテーブル４００のプロパティに違反しているか遵守しているかを検査する処理である。
【０１２４】
まず、プログラム状態を初期状態とし、初期状態をプログラム状態テーブル５００に記録する（ステップＳ２００１）。つぎに、現在のプログラム状態から未駆動である駆動可能なイベントが存在するか否かを判断する（ステップＳ２００２）。存在しない場合（ステップＳ２００２：Ｎｏ）、現在のプログラム状態が初期状態であるか否かを判断する（ステップＳ２００３）。初期状態でない場合（ステップＳ２００３：Ｎｏ）、プログラム状態を１イベント前の状態に戻して（ステップＳ２００４）、ステップＳ２００２に戻る。初期状態である場合（ステップＳ２００３：Ｙｅｓ）、モデル検査処理を終了して、ステップＳ１９０２に移行する。
【０１２５】
一方、未駆動である駆動可能なイベントが存在する場合（ステップＳ２００２：Ｙｅｓ）、未駆動である駆動可能なイベントを１つ選択して実行する（ステップＳ２００５）。そして、イベント駆動による遷移先のプログラム状態がすでに遷移したことがあるプログラム状態であるか否かを判断する（ステップＳ２００６）。まだ遷移したことがないプログラム状態である場合（ステップＳ２００６：Ｎｏ）、現在のプログラム状態をプログラム状態テーブル５００に記録する（ステップＳ２００７）。そして、直前のイベント駆動による状態遷移をプログラム状態遷移テーブル６００に記録する（ステップＳ２００８）。
【０１２６】
このあと、駆動イベントに関するプロパティのうち、事前条件が真で事後条件が偽となるプロパティがあるか否かを判断する（ステップＳ２００９）。該当するプロパティがない場合（ステップＳ２００９：Ｎｏ）、ステップＳ２００２に戻る。一方、該当するプロパティがある場合（ステップＳ２００９：Ｙｅｓ）、事前条件が真となり事後条件が偽となったプロパティを違反プロパティに決定し、違反プロパティテーブル８００に記録する（ステップＳ２０１２）。
【０１２７】
また、ステップＳ２００６において、イベント駆動による遷移先のプログラム状態がすでに遷移したことがあるプログラム状態である場合（ステップＳ２００６：Ｙｅｓ）、直前のイベント駆動による状態遷移をプログラム状態遷移テーブル６００に記録する（ステップＳ２０１０）。このあと、駆動イベントに関するプロパティのうち、事前条件が真で事後条件が偽となるプロパティがあるか否かを判断する（ステップＳ２０１１）。該当するプロパティがない場合（ステップＳ２０１１：Ｎｏ）、ステップＳ２００４に戻り、プログラム状態を１イベント前の状態に戻す。
【０１２８】
一方、該当するプロパティがある場合（ステップＳ２０１１：Ｙｅｓ）、事前条件が真となり事後条件が偽となったプロパティを違反プロパティに決定し、違反プロパティテーブル８００に記録する（ステップＳ２０１２）。ステップＳ２０１２のあと、初期状態から現在のプログラム状態へ至るプログラム状態遷移列を反例として記録する（ステップＳ２０１３）。このあと、ステップＳ１９０２に移行する。
【０１２９】
図２１は、図１９に示した正例検出処理（ステップＳ１９０４）の詳細な処理手順を示すフローチャートである。まず、反例中の正例チェック処理を実行する（ステップＳ２１０１）。反例中の正例チェック処理（ステップＳ２１０１）については、図２２で詳細に説明する。正例チェック後、反例中に正例が存在するか否かを判断する（ステップＳ２１０２）。存在する場合（ステップＳ２１０２：Ｙｅｓ）、正例の検出が成功したこととなり、ステップＳ１９０５に移行する。
【０１３０】
一方、正例が存在しない場合（ステップＳ２１０２：Ｎｏ）、プログラム状態を反例中最後のプログラム状態に設定し（ステップＳ２１０３）、プログラム状態を１イベント前の状態に戻す（ステップＳ２１０４）。そして、現在のプログラム状態がモデル検査の初期状態であるか否かを判断する（ステップＳ２１０５）。初期状態である場合（ステップＳ２１０５：Ｙｅｓ）、正例検出が失敗したこととなり、ステップＳ１９０５に移行する。
【０１３１】
一方、初期状態でない場合（ステップＳ２１０５：Ｎｏ）、現在のプログラム状態から修正対象プロパティに関するイベントが未駆動かつ駆動可能か否かを判断する（ステップＳ２１０６）。未駆動かつ駆動可能ではない場合（ステップＳ２１０６：Ｎｏ）、現在のプログラム状態から修正対象プロパティに関するイベント以外の他のイベントが未駆動かつ駆動可能か否かを判断する（ステップＳ２１０７）。
【０１３２】
他のイベントが未駆動かつ駆動可能でない場合（ステップＳ２１０７：Ｎｏ）、ステップＳ２１０４に戻って、プログラム状態を１イベント前の状態に戻す。一方、他のイベントが未駆動かつ駆動可能である場合（ステップＳ２１０７：Ｙｅｓ）、未駆動である駆動可能なイベントを駆動する（ステップＳ２１０８）。そして、ステップＳ２１１０に移行する。
【０１３３】
一方、ステップＳ２１０６において、現在のプログラム状態から修正対象プロパティに関するイベントが未駆動かつ駆動可能である場合（ステップＳ２１０６：Ｙｅｓ）、修正対象プロパティに関するイベントを駆動し（ステップＳ２１０９）、ステップＳ２１１０に移行する。ステップＳ２１１０では、イベント駆動による遷移先のプログラム状態がすでに遷移したことがあるプログラム状態であるか否かを判断する（ステップＳ２１１０）。
【０１３４】
すでに遷移したことがあるプログラム状態である場合（ステップＳ２１１０：Ｙｅｓ）、直前のイベント駆動による状態遷移をプログラム状態遷移テーブル６００に記録する（ステップＳ２１１１）。そして、直近のイベント前後で修正対象プロパティが真であるか否かを判断する（ステップＳ２１１２）。真でない場合（ステップＳ２１１２：Ｎｏ）、ステップＳ２１０４に戻り、プログラム状態を１イベント前の状態に戻す。一方、真である場合（ステップＳ２１１２：Ｙｅｓ）、初期状態から現在のプログラム状態に至るまでのプログラム状態遷移列を正例として記録する（ステップＳ２１１６）。これにより、正例が検出されたこととなり、ステップＳ１９０５に移行する。
【０１３５】
一方、ステップＳ２１１０において、まだ遷移していないプログラム状態である場合（ステップＳ２１１０：Ｎｏ）、現在のプログラム状態をプログラム状態テーブル５００に記録し（ステップＳ２１１３）、直前のイベント駆動による状態遷移をプログラム状態遷移テーブル６００に記録する（ステップＳ２１１４）。そして、直近のイベント前後で修正対象プログラムが真となるか否かを判断する（ステップＳ２１１５）。真となる場合（ステップＳ：２１１５Ｙｅｓ）、ステップＳ２１１６に移行する。一方、真でない場合（ステップＳ２１１５：Ｎｏ）、ステップＳ２１０６に戻る。
【０１３６】
図２２は、図２１に示した反例中の正例チェック処理（ステップＳ２１０１）の詳細な処理手順を示すフローチャートである。まず、プログラム状態をモデル検査開始時の状態とし（ステップＳ２２０１）、反例をすべてトレースしたか否かを判断する（ステップＳ２２０２）。すべてトレースしていない場合（ステップＳ２２０２：Ｎｏ）、反例にしたがってイベントを１つ駆動する（ステップＳ２２０３）。
【０１３７】
そして、直近のイベント前後で修正対象プロパティが真となるか否かを判断する（ステップＳ２２０４）。真でない場合（ステップＳ２２０４：Ｎｏ）、ステップＳ２２０２に戻る。一方、真である場合（ステップＳ２２０４：Ｙｅｓ）、初期状態から現在のプログラム状態に至るまでのプログラム状態遷移列を正例として記録する（ステップＳ２２０５）。そして、ステップＳ２１０２に移行する。一方、ステップＳ２２０２において、反例をすべてトレースした場合（ステップＳ２２０２：Ｙｅｓ）、反例の中から正例を取り出せなかったこととなり、ステップＳ２１０２に移行する。
【０１３８】
図２３は、図１９に示した差分論理式抽出処理（ステップＳ１９０７）の詳細な処理手順を示すフローチャートである。まず、差分状態遷移列中のすべてのイベントを確認したか否かを判断する（ステップＳ２３０１）。未確認のイベントがある場合（ステップＳ２３０１：Ｎｏ）、差分状態遷移列の中から未確認のイベントを１つ選択する（ステップＳ２３０２）。そして、修正対象プロパティを除き、選択したイベントに関するプロパティをすべて確認したか否かを判断する（ステップＳ２３０３）。
【０１３９】
すべて確認した場合（ステップＳ２３０３：Ｙｅｓ）、ステップＳ２３０１に戻る。一方、未確認のプロパティがある場合（ステップＳ２３０３：Ｎｏ）、修正対象プロパティを除き、選択したイベントに関するプロパティを１つ選択する（ステップＳ２３０４）。そして、選択したプロパティの事前条件を論理積標準形に変換する（ステップＳ２３０５）。
【０１４０】
このあと、論理積標準形の中の節をすべて分析したか否かを判断する（ステップＳ２３０６）。論理積標準形の中の節をすべて分析した場合（ステップＳ２３０６：Ｙｅｓ）、事前条件の場合と同様、選択したプロパティの事後条件を論理積標準形に変換して各節の分析をおこなう。そして、差分論理式テーブル９００に追加する（ステップＳ２３０７）。このあと、ステップＳ２３０３に戻る。
【０１４１】
一方、未分析の節がある場合（ステップＳ２３０６：Ｎｏ）、未分析の節を１つ選択する（ステップＳ２３０８）。そして、選択した節の中のすべての原子論理式を要素とする論理式集合を作る（ステップＳ２３０９）。そして、論理式集合のべき集合を作る（ステップＳ２３１０）。べき集合とは、ある集合のすべての部分集合をその要素とする集合である。
【０１４２】
図２４は、論理式集合とそのべき集合を示す説明図である。ステップＳ２３１０のあと、べき集合中の要素である部分論理式集合をすべて分析したか否かを判断する（ステップＳ２３１１）。未分析の部分論理式集合がある場合（ステップＳ２３１１：Ｎｏ）、未分析の部分論理式集合を選択する（ステップＳ２３１２）。
【０１４３】
そして、選択した部分論理式集合の全要素をＯＲで結合した論理式（節）を差分論理式として差分論理式テーブル９００に追加し（ステップＳ２３１３）、ステップＳ２３１１に戻る。ステップＳ２３１１において、すべて分析した場合（ステップＳ２３１１：Ｙｅｓ）、ステップＳ２３０６に戻る。また、ステップＳ２３０１において、差分状態遷移列の中のすべてのイベントを確認した場合（ステップＳ２３０１：Ｙｅｓ）、ステップＳ１９０８に移行する。
【０１４４】
図２５は、図１９に示した候補論理式抽出処理（ステップＳ１９０９）の詳細な処理手順を示すフローチャートである。まず、正例と反例それぞれの最後のイベント実施直前のプログラム状態を取得する（ステップＳ２５０１）。そして、差分論理式をすべてチェックしたか否かを判断する（ステップＳ２５０２）。
【０１４５】
未チェックの差分論理式がある場合（ステップＳ２５０２：Ｎｏ）、未チェックの差分論理式を１つ選択し（ステップＳ２５０３）、選択した差分論理式の真偽判定を、正例側のプログラム状態と反例側のプログラム状態とに対して実行する（ステップＳ２５０４）。このあと、正例側と反例側とで真偽が異なるか否かを判断する（ステップＳ２５０５）。
【０１４６】
真偽が同一である場合（ステップＳ２５０５：Ｎｏ）、ステップＳ２５０２に戻る。一方、真偽が異なる場合（ステップＳ２５０５：Ｙｅｓ）、選択した差分論理式を候補論理式に決定して候補論理式テーブル１０００に記録する（ステップＳ２５０６）。このあと、選択した差分論理式は正例側で真となるか否かを判断する（ステップＳ２５０７）。真である場合（ステップＳ２５０７：Ｙｅｓ）、ＮＯＴ付加フラグを「付加しない」に設定して（ステップＳ２５０８）、ステップＳ２５０２に移行する。
【０１４７】
一方、偽である場合（ステップＳ２５０７：Ｎｏ）、ＮＯＴ付加フラグを「付加する」に設定して（ステップＳ２５０９）、ステップＳ２５０２に移行する。このあと、ステップＳ２５０２において、差分論理式をすべてチェックした場合（ステップＳ２５０２：Ｙｅｓ）、候補論理式の生成を終了してステップＳ１９１０に移行する。
【０１４８】
図２６は、図１９に示した候補論理式追加によるプロパティ修正処理（ステップＳ１９１１）の詳細な処理手順を示すフローチャートである。まず、修正対象プロパティを修正済プロパティの初期値とする（ステップＳ２６０１）。つぎに、追加対象として、候補論理式を１つ以上選択する（ステップＳ２６０２）。
【０１４９】
そして、追加対象の候補論理式をすべて追加したか否かを判断する（ステップＳ２６０３）。すべて追加していない場合（ステップＳ２６０３：Ｎｏ）、未追加である追加対象の候補論理式を１つ選択する（ステップＳ２６０４）。このあと、選択した候補論理式に対応する候補論理式テーブル１０００中のＮＯＴ付加フラグが「付加する」であるか否かを判断する（ステップＳ２６０５）。
【０１５０】
「付加する」である場合（ステップＳ２６０５：Ｙｅｓ）、選択した候補論理式の否定を現時点での修正済プロパティの事前条件に、ＡＮＤで追加する（ステップＳ２６０６）。そして、ステップＳ２６０３に戻る。一方、「付加する」でない場合（ステップＳ２６０５：Ｎｏ）、選択した候補論理式を現時点での修正済プロパティの事前条件にＡＮＤで追加する（ステップＳ２６０７）。そして、ステップＳ２６０３に戻る。また、ステップＳ２６０３において、追加対象の候補論理式をすべて追加した場合（ステップＳ２６０３：Ｙｅｓ）、修正処理を終了してステップＳ１９１２に移行する。
【０１５１】
このように、実施の形態１によれば、検査対象プログラムのモデル検査においてプロパティ違反が発生した場合、正例・反例に関する情報と既存のプロパティを利用して、正例の維持および反例のガードをしながらプロパティの事前条件を修正することができる。したがって、既存のプロパティ中に存在する論理式を追加するだけで事前条件不足を解消することができる。これにより、従来のように、述語・関数の雛形から修正条件を生成する作業を行う必要がないため、膨大な作業量・記憶領域を必要とすることなく、プロパティを適正に修正することができる。
【０１５２】
＜実施の形態２＞
つぎに、実施の形態２について説明する。実施の形態２では、モデル検査の結果プロパティ違反が発生した場合、違反プロパティから修正対象プロパティを１つ選択する。そして、検査対象プログラムの可能なすべての状態遷移に対して、選択された修正対象プロパティに関する全反例および全正例を検出する。このあと、検出された反例のすべてをガードし、検出された正例のすべてを維持するように修正対象プロパティの修正を実行する。これにより、修正済プロパティを得る。
【０１５３】
なお、実施の形態２では、実施の形態１と異なる部分について説明し、実施の形態１との重複部分については説明を省略する。たとえば、図２に示したハードウェア構成については同一であるため、省略する。
【０１５４】
また、実施の形態２におけるプログラム状態遷移中には、あらたにＬ１およびＬ２というイベントが出現する。イベントＬ１，Ｌ２は、ログイン画面３０１（プログラム状態Ｓ１）において「ｓｏｆｔ」である会員ＩＤをそれぞれ「ｔｅｓｔ」、「ｔｅｓｔ＿２」に変更するイベントである。プログラム状態Ｓ１においてイベントＬ１駆動後のプログラム状態をＳ１’、プログラム状態Ｓ１においてイベントＬ２駆動後のプログラム状態をＳ１”と表記する。
【０１５５】
（各種テーブルの記憶内容）
まず、実施の形態２で用いる各種テーブルの記憶内容について説明する。実施の形態２では、実施の形態１で用いたプロパティテーブル４００、プログラム状態テーブル５００、プログラム状態遷移テーブル６００、違反プロパティテーブル８００、差分論理式テーブル９００、候補論理式テーブル１０００のほか、反例テーブル、正例テーブル、および比較済み正例テーブルを用いる。これらテーブルは、具体的には、たとえば、図２に示したＲＯＭ２０２、ＲＡＭ２０３、磁気ディスク２０５、光ディスク２０７などの記憶装置に記憶される。以下、順に説明する。
【０１５６】
図２７−１は、反例テーブルの記憶内容を示す説明図である。反例テーブル２７０１とは、ガード対象となるすべての反例を保持するテーブルである。具体的には、反例名と、反例内容（プログラム状態遷移列）とをフィールド項目とし、反例ごとにレコードを有する。反例名とは、反例を一意に特定する識別子である。反例テーブル２７０１は初期状態では空であるが、反例が検出される都度、順次追加される。
【０１５７】
図２７−２は、正例テーブルの記憶内容を示す説明図である。正例テーブル２７０２とは、維持対象となるすべての正例を保持するテーブルである。具体的には、正例名と、正例内容（プログラム状態遷移列）とをフィールド項目とし、正例ごとにレコードを有する。正例名とは、正例を一意に特定する識別子である。正例テーブル２７０２は初期状態では空であるが、正例が検出される都度、順次追加される。
【０１５８】
図２８は、比較済み正例テーブル２８００の記憶内容を示す説明図である。比較済み正例テーブル２８００とは、１つの反例について、どの正例との差分に対してプロパティの修正を試みたかを記録するテーブルである。具体的には、正例名と、比較済みフラグとをフィールド項目とし、正例ごとにレコードを有する。
【０１５９】
ここで、比較済みフラグとは、対応する正例と反例の差分に対してプロパティの修正を試みたかどうかを示すフラグである。たとえば、図２８に示した内容では、現在修正中の反例について、正例１との差分に対してプロパティの修正を試みたが正例２との差分に対してはまだプロパティの修正を試みていないことを示している。
【０１６０】
つぎに、図１１に示した実施の形態１の機能のうち実施の形態１とは異なる機能について説明する。実施の形態２では、プログラム状態遷移中に存在するすべての反例をガードし、全正例を維持するようプロパティ修正を実行する。検査部１１０１は実施の形態１と同じであるが、検出部１１０２は、実施の形態１と実施の形態２とでは異なる。実施の形態２の検出部１１０２では、プログラム状態遷移中のすべての反例・正例を検出する機能を有する。
【０１６１】
図２９は、実施の形態２にかかる検出部１１０２による反例・正例検出例を示す説明図である。図２９では、検証対象プログラムのプログラム状態遷移列において、プロパティＰ＿Ｅ６＿２に対する正例と反例を示している。検出部１１０２は、検査対象プログラムの実行可能なすべての状態遷移を実行して全反例の検出を行う。
【０１６２】
具体的には、すでに検出した反例「反１」に加えて反例「Ｓ１（Ｌ１）→Ｓ１’（Ｅ１）→Ｓ１０（Ｅ４）→Ｓ１１（Ｅ５）→Ｓ１２（Ｅ２）→Ｓ１３（Ｅ６）→Ｓ１４」が検出される。この反例は、「反２」として反例テーブル２７０１に登録される。
【０１６３】
「反２」を言い換えると、ログイン画面３０１（プログラム状態Ｓ１）からイベントＬ１を駆動して会員ＩＤを「ｔｅｓｔ」に変更したログイン画面３０１（プログラム状態Ｓ１’）に至る。つぎに、イベントＥ１を駆動してメニュー画面３０２（プログラム状態Ｓ１０）に至る。つぎに、イベントＥ４を駆動してアンケート画面３０４（プログラム状態Ｓ１１）に至る。つぎに、イベントＥ５を駆動してメニュー画面３０２（プログラム状態Ｓ１２）に至る。つぎに、イベントＥ２を駆動して商品選択画面３０３（プログラム状態Ｓ１３）に至る。つぎに、イベントＥ６を駆動して支払い確認画面３０５（プログラム状態Ｓ１４）に至る。
【０１６４】
このように、「反２」はプログラム状態Ｓ１〜Ｓ１４までのプログラム状態遷移列である。「反２」では、プログラム状態Ｓ１３においてプロパティＰ＿Ｅ６＿２の事前条件（「画面．会員種別」＝正会員）が真になり、また、プログラム状態Ｓ１４でプロパティＰ＿Ｅ６＿２の事後条件（「画面．サービス」＝「サービスなし」）が偽になる。
【０１６５】
そして、検査対象プログラムの実行可能なすべての状態遷移を実行した結果、全反例の検出終了後には、プログラム状態Ｓ１〜Ｓ１８、Ｓ１’、Ｓ１”がプログラム状態テーブル５００に保持される。また、以下のプログラム状態遷移がプログラム状態遷移テーブル６００に保持される。
【０１６６】
Ｓ１（Ｅ１）→Ｓ２
Ｓ２（Ｅ４）→Ｓ３
Ｓ３（Ｅ５）→Ｓ４
Ｓ４（Ｅ２）→Ｓ５
Ｓ５（Ｅ６）→Ｓ６
Ｓ５（Ｅ３）→Ｓ４
Ｓ４（Ｅ４）→Ｓ７
Ｓ７（Ｅ５）→Ｓ４
Ｓ２（Ｅ２）→Ｓ８
Ｓ８（Ｅ６）→Ｓ９
Ｓ８（Ｅ３）→Ｓ２
Ｓ１（Ｌ１）→Ｓ１’
Ｓ１’（Ｅ１）→Ｓ１０
Ｓ１０（Ｅ４）→Ｓ１１
Ｓ１１（Ｅ５）→Ｓ１２
Ｓ１２（Ｅ２）→Ｓ１３
Ｓ１３（Ｅ６）→Ｓ１４
Ｓ１（Ｌ２）→Ｓ１”
Ｓ１”（Ｅ１）→Ｓ１５
Ｓ１５（Ｅ４）→Ｓ１６
Ｓ１６（Ｅ５）→Ｓ１７
Ｓ１７（Ｅ２）→Ｓ１８
Ｓ１８（Ｅ６）→Ｓ１９
【０１６７】
また、検出部１１０２は、検査対象プログラムの実行可能なすべての状態遷移を実行して全正例の検出を行う。具体的には、実施の形態１で検出した正例「Ｓ１（Ｅ１）→Ｓ２（Ｅ２）→Ｓ８（Ｅ６）→Ｓ９」を検出して「正１」として正例テーブル２７０２に追加する。加えて、正例「Ｓ１（Ｌ２）→Ｓ１”（Ｅ１）→Ｓ１５（Ｅ４）→Ｓ１６（Ｅ５）→Ｓ１７（Ｅ２）→Ｓ１８（Ｅ６）→Ｓ１９」を検出して、「正２」として正例テーブル２７０２に追加する。
【０１６８】
「正２」を言い換えると、ログイン画面３０１（プログラム状態Ｓ１）からイベントＬ２を駆動して会員ＩＤを「ｔｅｓｔ＿２」に変更したログイン画面３０１（プログラム状態Ｓ１”）に至る。つぎに、イベントＥ１を駆動してメニュー画面３０２（プログラム状態Ｓ１５）に至る。つぎに、イベントＥ４を駆動してアンケート画面３０４（プログラム状態Ｓ１６）に至る。つぎに、イベントＥ５を駆動してメニュー画面３０２（プログラム状態Ｓ１７）に至る。つぎに、イベントＥ２を駆動して商品選択画面３０３（プログラム状態Ｓ１８）に至る。つぎに、イベントＥ６を駆動して支払い確認画面３０５（プログラム状態Ｓ１９）に至る状態遷移列である。
【０１６９】
このように、「正２」はプログラム状態Ｓ１〜Ｓ１９までのプログラム状態遷移列である。プログラム状態Ｓ１８においてプロパティＰ＿Ｅ６＿２の事前条件（「画面．会員種別」＝正会員）が真になり、また、プログラム状態Ｓ１９でプロパティＰ＿Ｅ６＿２の事後条件（「画面．サービス」＝「サービスなし」）が真になる。また、比較済み正例テーブル２８００には、正例「正１」および「正２」が登録され、「正１」の比較済みフラグは「比較済み」、「正２」の比較済みフラグは「未比較」となっている。
【０１７０】
また、図１１に示した差分抽出部１１０３は、実施の形態２では、反例テーブル２７０１から反例を１つ選び、さらに正例テーブル２７０２から正例を１つ選び、差分抽出を実行する。差分抽出の処理内容自体は実施の形態１と同じである。
【０１７１】
図３０は、実施の形態２にかかる反例側差分と正例側差分との抽出例を示す説明図である。実施の形態２でも、正例側差分を差分状態遷移列として利用する。反例側差分は利用しない。図３０では、正例「正１」と反例「反１」とを選択して差分を抽出した例である。なお、差分論理式の抽出については、実施の形態１と同じであるため省略する。
【０１７２】
また、図１１に示した生成部１１０５は、実施の形態２では、差分論理式から選択した反例をガードして全正例を維持する候補論理式を抽出し、候補論理式の一部を不足条件として選択する。不足条件を追加することで選択した反例に関して事前条件不足を解消させる。
【０１７３】
図３１は、実施の形態２にかかる候補論理式の生成例を示す説明図である。実施の形態２では、以下の条件を満足する差分論理式が、候補論理式となる。
条件：全正例における修正対象プロパティの評価イベント駆動直前のプログラム状態での評価結果が同じで、かつ反例における修正対象のプロパティ評価イベント駆動直前のプログラム状態での評価結果が正例側と異なること。
【０１７４】
候補論理式が得られなかった場合、比較済み正例テーブル２８００において、比較済みフラグが未比較の正例を選択し、再度、差分論理式および候補論理式の抽出を試みる。また、候補論理式テーブル１０００では、差分論理式の評価結果において正例側がすべて偽で反例側が真である場合、ＮＯＴ付加フラグを「付加する」に設定する。したがって、候補論理テーブルから差分１を選択した場合、修正対象プロパティの事前条件には、差分１の否定である
「ＮＯＴ（会員情報（累計ポイント，画面．会員ＩＤ）＞＝５０００）」
がＡＮＤで追加される。
【０１７５】
図１１に示した修正部１１０６は、実施の形態２では、現在の候補論理式および修正対象プロパティから選択した反例をガードする修正後のプロパティを生成する機能に加え、現在の修正で全反例がガードされているかチェックする。まだガードされていない反例が存在する場合には、その反例に対して、差分抽出部１１０３による反例と正例の差分の抽出、差分論理式抽出部１１０４および生成部１１０５による差分状態遷移列から不足条件の抽出をおこなって、再度修正をおこなう。
【０１７６】
また、修正部１１０６は、具体的には、ガードされた反例すべてを反例テーブル２７０１から除去する。もし反例テーブル２７０１が空になれば、全反例がガードされているため、プロパティ修正が完了する。反例テーブル２７０１が空でない場合、反例テーブル２７０１の反例はガードされていないので、ガードされていない反例を１つ選び、各正例に対して、差分抽出部１１０３による反例と正例の差分の抽出、差分論理式抽出部１１０４および生成部１１０５による差分状態遷移列から不足条件の抽出をおこなって、再度修正をおこなう。
【０１７７】
図３２−１〜図３２−６は、実施の形態２にかかる修正対象プロパティの修正例を示す説明図である。図３２−１では、正例である「正１」，「正２」と反例である「反１」，「反２」に対して差分１を追加して修正をおこなう。差分１を追加することで、反例「反１」はガードされたが、「反２」はガードされていない。この状態では、反例「反１」はガード済みであるため、反例テーブル２７０１から「反１」のレコードを削除する。このあと、図３２−２に移行する。
【０１７８】
図３２−２では、ガードされなかった反例「反２」を選択し、比較済み正例テーブル２８００を初期化する。すなわち、比較済みフラグがいずれの正例も「未比較」状態となる。この状態で、正例「正１」を選択し、「正１」と「反２」とで差分論理式を抽出する。差分論理式を抽出すると、比較済み正例テーブル２８００のうち「正１」の比較済みフラグを「比較済み」に更新する。
【０１７９】
この場合の差分状態遷移列は、正例「正１」自身となるため、イベントＥ１，Ｅ２，Ｅ６に関するプロパティから差分論理式を得る。図３２−２には、抽出された差分論理式が登録された差分論理式テーブル９００を示している。このあと、図３２−３に移行する。
【０１８０】
図３２−３では、図３２−２で得られた差分論理式テーブル９００中の各差分論理式を「正１」、「反１」、「反２」で評価して、差分論理式評価結果を得る。そして、候補論理式を抽出する。
【０１８１】
図３２−３の差分論理式評価結果では、すべての正例が真で反例が偽、または、すべての正例が偽で反例が真となる結果が得られなかったので、候補論理式は選ばれない。したがって、この段階での修正対象プロパティの事前条件は、図３２−２に示したとおりとなる。このあと、図３２−４に移行する。
【０１８２】
図３２−４では、正例「正２」を選択して、「正２」と「反２」とで差分論理式を抽出する。差分論理式を抽出すると、比較済み正例テーブル２８００のうち「正２」の比較済みフラグを「比較済み」に更新する。
【０１８３】
この場合の差分状態遷移列は、正例「正２」自身となるため、イベントＬ２，Ｅ１，Ｅ２，Ｅ４〜Ｅ６に関するプロパティから差分論理式を得る。図３２−４には、抽出された差分論理式が登録された差分論理式テーブル９００を示している。このあと、図３２−５に移行する。
【０１８４】
図３２−５では、図３２−４で得られた差分論理式テーブル９００から候補論理式を抽出する。そして、差分論理式を、「正１」、「正２」、「反２」で評価して、差分論理式評価結果を得る。
【０１８５】
図３２−５の差分論理式評価結果では、差分９について、すべての正例が真で反例が偽と評価され、差分１０について、すべての正例が偽で反例が真と評価される。したがって、差分９と差分１０が候補論理式となり、候補論理式テーブル１０００に記録される。
【０１８６】
また、すべての正例が真で反例が偽と評価された候補論理式（ここでは差分９）については、ＮＯＴ付加フラグが「付加しない」に設定される。すべての正例が偽で反例が真と評価された候補論理式（ここでは差分１０）については、ＮＯＴ付加フラグが「付加する」に設定される。この時点での修正対象プロパティの事前条件は、図３２−５に示すとおりである。このあと、修正部１１０６により差分９を事前条件に追加する。追加後の修正対象プロパティの事前条件は、図３２−５に示すとおりである。このあと、図３２−６に移行する。
【０１８７】
図３２−６では、図３２−５において反例「反２」については修正対象プロパティに差分９をＡＮＤ追加してガードされたため、反例テーブル２７０１から「反２」を削除する。これにより、反例テーブル２７０１は空になる。「反２」のガード時点での修正対象プロパティは、図３２−６に示すとおりである。反例テーブルが空であるため、修正処理が完了し、「反２」のガード時点での修正対象プロパティが最終的に出力される修正済プロパティである。
【０１８８】
図３３は、図３２−６で得られた修正済プロパティの事前条件の真偽を示す説明図である。図３３において、修正済プロパティの事前条件は、プログラム状態Ｓ５，Ｓ１３（反例側）で偽となり、プログラム状態Ｓ８，Ｓ１８（正例側）で真となる。これにより、図３２−１〜図３２−６に示した修正例では、検出した全反例をガードして検出した全正例を維持する修正済プロパティが得られていることがわかる。
【０１８９】
（反例解析処理手順）
図３４および図３５は、実施の形態２にかかるプロパティ修正装置による反例解析処理手順を示すフローチャートである。まず、検査部１１０１によりモデル検査処理を実行する（ステップＳ３４０１）。モデル検査処理（ステップＳ３４０１）については、図２０に示したモデル検査処理（ステップＳ１９０１）と同一処理である。
【０１９０】
つぎに、モデル検査処理の検査結果に違反プロパティがあるか否かを判断する（ステップＳ３４０２）。違反プロパティがない場合（ステップＳ３４０２：Ｎｏ）、プロパティを修正する必要がないため、ステップＳ３４０９に移行する。
【０１９１】
一方、違反プロパティがある場合（ステップＳ３４０２：Ｙｅｓ）、違反プロパティを修正対象プロパティとして１つ選択する（ステップＳ３４０３）。そして、検出部１１０２により全反例検出処理を実行する（ステップＳ３４０４）。全反例検出処理（ステップＳ３４０４）については、図３６で後述する。つぎに、検出部１１０２により全正例検出処理を実行する（ステップＳ３４０５）。全正例検出処理（ステップＳ３４０５）については、図３７で後述する。
【０１９２】
そして、全正例検出処理（ステップＳ３４０５）で正例が検出されたか否かを判断する（ステップＳ３４０６）。正例が検出されなかった場合（ステップＳ３４０６：Ｎｏ）、出力部１１０７によりＮＧ出力（修正失敗）をおこない（ステップＳ３４０７）、一連の処理を終了する。
【０１９３】
一方、正例が検出された場合（ステップＳ３４０６：Ｙｅｓ）、反例テーブル２７０１が空であるか否かを判断する（ステップＳ３４０８）。空でない場合（ステップＳ３４０８：Ｎｏ）、図３５のステップＳ３５０１に移行する。一方、空である場合（ステップＳ３４０８：Ｙｅｓ）、ステップＳ３４０９に移行する。ステップＳ３４０９では、出力部１１０７により結果出力（修正済プロパティや修正不要通知）をおこない（ステップＳ３４０９）、一連の処理を終了する。
【０１９４】
反例テーブル２７０１が空でない場合（ステップＳ３４０８：Ｎｏ）、図３５において、反例を選択し（ステップＳ３５０１）、比較済み正例テーブル２８００を初期化する（ステップＳ３５０２）。そして、未比較の正例があるかを比較済み正例テーブル２８００を参照して判断する（ステップＳ３５０３）。未比較の正例がない場合（ステップＳ３５０３：Ｎｏ）、出力部１１０７によりＮＧ出力（修正失敗）をおこない（ステップＳ３５０４）、一連の処理を終了する。
【０１９５】
一方、未比較の正例がある場合（ステップＳ３５０３：Ｙｅｓ）、未比較の正例を選択し（ステップＳ３５０５）、選択した正例について比較済み正例テーブル２８００の比較済みフラグを「比較済み」に更新する（ステップＳ３５０６）。つぎに、選択した正例と反例との差分を差分抽出部１１０３により実行する（ステップＳ３５０７）。そして、差分論理式抽出部１１０４により、差分論理式抽出処理を実行する（ステップＳ３５０８）。差分論理式抽出処理（ステップＳ３５０８）は、実施の形態１の差分論理式抽出処理（ステップＳ１９０７）と同一処理である。
【０１９６】
そして、差分論理式があるか否かを判断する（ステップＳ３５０９）。差分論理式がない場合（ステップＳ３５０９：Ｎｏ）、ステップＳ３５０３に戻り、未比較の正例を選択しなおす。一方、差分論理式がある場合（ステップＳ３５０９：Ｙｅｓ）、生成部１１０５により候補論理式生成処理を実行する（ステップＳ３５１０）。候補論理式生成処理（ステップＳ３５１０）については、図３８で後述する。
【０１９７】
このあと、候補論理式があるか否かを判断する（ステップＳ３５１１）。候補論理式がない場合（ステップＳ３５１１：Ｎｏ）ステップＳ３５０３に戻り、未比較の正例を選択しなおす。一方、候補論理式がある場合（ステップＳ３５１１：Ｙｅｓ）、候補論理式追加によるプロパティ修正処理を実行する（ステップＳ３５１２）。候補論理式追加によるプロパティ修正処理（ステップＳ３５１２）は、実施の形態１の候補論理式追加によるプロパティ修正処理（ステップＳ１９１１）と同一処理である。
【０１９８】
このあと、修正処理（ステップＳ３５１２）によりガードされた反例を反例テーブル２７０１から除去して（ステップＳ３５１３）、図３４のステップＳ３４０８に戻り、反例テーブル２７０１が空であるかを判断することとなる。
【０１９９】
図３６は、図３４に示した全反例検出処理（ステップＳ３４０４）の詳細な処理手順を示すフローチャートである。まず、プログラム状態をモデル検査開始時の状態とし（ステップＳ３６０１）、現在のプログラム状態から一連の全反例検出処理において未駆動の駆動可能なイベントが存在するか否かを判断する（ステップＳ３６０２）。未駆動の駆動可能なイベントが存在する場合（ステップＳ３６０２：Ｙｅｓ）、未駆動の駆動可能なイベントを１つ選択して駆動する（ステップＳ３６０３）。
【０２００】
そして、駆動したイベントが修正対象プロパティに対するイベントであるか否かを判断する（ステップＳ３６０４）。修正対象プロパティに対するイベントである場合（ステップＳ３６０４：Ｙｅｓ）、駆動したイベントの前後で修正対象プロパティが違反するか否かを判断する（ステップＳ３６０５）。違反する場合（ステップＳ３６０５：Ｙｅｓ）、初期状態から現在のプロパティ違反に至るプログラム状態遷移列がすでに反例テーブル２７０１に存在するか否かを判断する（ステップＳ３６０６）。
【０２０１】
存在しない場合（ステップＳ３６０６：Ｎｏ）、初期状態から現在のプロパティ違反に至る状態遷移列を反例テーブル２７０１に追加して（ステップＳ３６０７）、ステップＳ３６０８に移行する。一方、初期状態から現在のプロパティ違反に至るプログラム状態遷移列がすでに反例テーブル２７０１に存在する場合（ステップＳ３６０６：Ｙｅｓ）、ステップＳ３６０８に移行する。また、ステップＳ３６０５において、修正対象プロパティが違反しない場合（ステップＳ３６０５：Ｎｏ）、ステップＳ３６０８に移行する。
【０２０２】
ステップＳ３６０８において、現在のプログラム状態が、一連の全反例検出処理においてすでに遷移したことのあるプログラム状態であるか否かを判断する（ステップＳ３６０８）。遷移したことがないプログラム状態である場合（ステップＳ３６０８：Ｎｏ）、現在のプログラム状態をプログラム状態テーブル５００に上書き記録して（ステップＳ３６０９）、直前のイベント駆動による状態遷移をプログラム状態遷移テーブル６００に上書き記録する（ステップＳ３６１０）。そして、プログラム状態を１イベント前の状態に戻して（ステップＳ３６１１）、ステップＳ３６０２に戻る。なお、プログラム状態テーブル５００への上書き記録とは、記録しようとしているプログラム状態と変数状態が全く同じプログラム状態がすでに記録されている場合は、新たに記録することを避けるようにプログラム状態テーブル５００への記録を行うことを指す。また、プログラム状態遷移テーブル６００への上書き記録とは、記録しようとしている状態遷移と全く同じイベント前状態、駆動イベント、イベント後状態を持つ状態遷移がすでに記録されている場合は、新たに記録することを避けるようにプログラム状態遷移テーブル６００への記録を行うことを指す。
【０２０３】
一方、現在のプログラム状態がすでに遷移したことのあるプログラム状態である場合（ステップＳ３６０８：Ｙｅｓ）、直前のイベント駆動による状態遷移をプログラム状態遷移テーブル６００に上書き記録する（ステップＳ３６１０）。そして、プログラム状態を１イベント前の状態に戻して（ステップＳ３６１１）、ステップＳ３６０２に戻る。
【０２０４】
ステップＳ３６０２において、現在のプログラム状態から未駆動の駆動可能なイベントが存在しない場合（ステップＳ３６０２：Ｎｏ）、プログラム状態が検査開始時の状態（初期状態）であるか否かを判断する（ステップＳ３６１２）。検査開始時の状態でない場合（ステップＳ３６１２：Ｎｏ）、ステップＳ３６１１に戻って１イベント前に戻す。一方、検査開始時の状態である場合（ステップＳ３６１２：Ｙｅｓ）、全反例検出処理を終了する。
【０２０５】
図３７は、図３４に示した全正例検出処理（ステップＳ３４０５）の詳細な処理手順を示すフローチャートである。まず、プログラム状態をモデル検査開始時の状態とし（ステップＳ３７０１）、現在のプログラム状態から一連の全正例検出処理において未駆動の駆動可能なイベントが存在するか否かを判断する（ステップＳ３７０２）。未駆動の駆動可能なイベントが存在する場合（ステップＳ３７０２：Ｙｅｓ）、未駆動の駆動可能なイベントを１つ選択して駆動する（ステップＳ３７０３）。
【０２０６】
そして、駆動したイベントが修正対象プロパティに対するイベントであるか否かを判断する（ステップＳ３７０４）。修正対象プロパティに対するイベントでない場合（ステップＳ３７０４：Ｎｏ）、ステップＳ３７０８に移行する。一方、修正対象プロパティに対するイベントである場合（ステップＳ３７０４：Ｙｅｓ）、駆動したイベントの前後で修正対象プロパティの事前条件・事後条件がともに真となるか否かを判断する（ステップＳ３７０５）。ともに真とならない場合（ステップＳ３７０５：Ｎｏ）、ステップＳ３７０８に移行する。
【０２０７】
一方、ともに真である場合（ステップＳ３７０５：Ｙｅｓ）、初期状態から現在のプログラム状態に至るプログラム状態遷移列を正例テーブル２７０２に追加する（ステップＳ３７０６）。そして、比較済み正例テーブル２８００に正例を追加して（ステップＳ３７０７）、ステップＳ３７０８に移行する。
【０２０８】
ステップＳ３７０８では、現在のプログラム状態が、一連の全正例検出処理においてすでに遷移したことのあるプログラム状態であるか否かを判断する（ステップＳ３７０８）。遷移したことがないプログラム状態である場合（ステップＳ３７０８：Ｎｏ）、ステップＳ３７０２に戻る。
【０２０９】
一方、現在のプログラム状態がすでに遷移したことのあるプログラム状態である場合（ステップＳ３７０８：Ｙｅｓ）、プログラム状態を１イベント前の状態に戻して（ステップＳ３７０９）、ステップＳ３７０２に戻る。
【０２１０】
ステップＳ３７０２において、現在のプログラム状態から未駆動の駆動可能なイベントが存在しない場合（ステップＳ３７０２：Ｎｏ）、プログラム状態が検査開始時の状態（初期状態）であるか否かを判断する（ステップＳ３７１０）。検査開始時の状態でない場合（ステップＳ３７１０：Ｎｏ）、ステップＳ３７０９に戻って１イベント前に戻す。一方、検査開始時の状態である場合（ステップＳ３７１０：Ｙｅｓ）、全正例検出処理を終了して、ステップＳ３４０６へ戻る。
【０２１１】
図３８は、図３５に示した候補論理式生成処理（ステップＳ３５１０）の詳細な処理手順を示すフローチャートである。まず、正例と反例それぞれの最後のイベント実施直前のプログラム状態を取得する（ステップＳ３８０１）。そして、差分論理式をすべてチェックしたか否かを判断する（ステップＳ３８０２）。
【０２１２】
未チェックの差分論理式がある場合（ステップＳ３８０２：Ｎｏ）、未チェックの差分論理式を１つ選択し（ステップＳ３８０３）、選択した差分論理式の真偽判定を、正例側のプログラム状態と反例側のプログラム状態とに対して実行する（ステップＳ３８０４）。そして、全正例において真偽が一致するか否かを判断する（ステップＳ３８０５）。不一致の場合（ステップＳ３８０５：Ｎｏ）、ステップＳ３８０２に戻る。一方、一致する場合（ステップＳ３８０５：Ｙｅｓ）、正例側と反例側とで真偽が異なるか否かを判断する（ステップＳ３８０６）。
【０２１３】
真偽が同一である場合（ステップＳ３８０６：Ｎｏ）、ステップＳ３８０２に戻る。一方、真偽が異なる場合（ステップＳ３８０６：Ｙｅｓ）、選択した差分論理式を候補論理式に決定して候補論理式テーブル１０００に記録する（ステップＳ３８０７）。このあと、選択した差分論理式が正例側で真となるか否かを判断する（ステップＳ３８０８）。真である場合（ステップＳ３８０８：Ｙｅｓ）、ＮＯＴ付加フラグを「付加しない」に設定して（ステップＳ３８０９）、ステップＳ３８０２に移行する。
【０２１４】
一方、偽である場合（ステップＳ３８０８：Ｎｏ）、ＮＯＴ付加フラグを「付加する」に設定して（ステップＳ３８１０）、ステップＳ３８０２に移行する。このあと、ステップＳ３８０２において、差分論理式をすべてチェックした場合（ステップＳ３８０２：Ｙｅｓ）、候補論理式の生成を終了してステップＳ３５１１に移行する。
【０２１５】
このように、実施の形態２によれば、全正例を維持しつつ選択された反例をガードする修正済プロパティを生成し、その修正済プロパティを、さらに修正対象プロパティに置き換える。そして、再びガードされていない反例と全正例から選ばれた正例との差分を抽出して、再帰的に実行する。これにより、最終的に全正例を維持しつつ全反例をガードする修正済プロパティを得ることができる。
【０２１６】
すなわち、検査対象プログラムのモデル検査においてプロパティ違反が発生した場合、正例・反例に関する情報と既存のプロパティを利用して、正例の維持および反例のガードをしながらプロパティの事前条件を修正することができる。したがって、既存のプロパティ中に存在する論理式を追加するだけで事前条件不足を解消することができる。これにより、従来のように、述語・関数の雛形から修正条件を生成する作業を行う必要がないため、膨大な作業量・記憶領域を必要とすることなく、プロパティを適正に修正することができる。
【０２１７】
以上のことから、正例と反例の正例側差分状態遷移列中で駆動されたイベントに関するプロパティから正例の維持と反例のガードという修正対象プロパティの事前条件不足解消の要件を満たす条件を生成・追加することで、プロパティの事前条件が修正可能になる。
【０２１８】
この際、述語・関数の雛形を用いて条件式の候補を生成するという作業は不要である。よって，当該状況においては、従来のような条件式の候補生成のための膨大な作業および記憶領域の必要なく、事前条件不足を解消したプロパティを得ることができる。
【０２１９】
なお、本実施の形態で説明したプロパティ修正方法は、予め用意されたプログラムをパーソナル・コンピュータやワークステーション等のコンピュータで実行することにより実現することができる。本プロパティ修正プログラムは、ハードディスク、フレキシブルディスク、ＣＤ−ＲＯＭ、ＭＯ、ＤＶＤ等のコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。また本プロパティ修正プログラムは、インターネット等のネットワークを介して配布してもよい。
【０２２０】
上述した実施の形態に関し、さらに以下の付記を開示する。
【０２２１】
（付記１）検査対象プログラムで駆動されるイベントごとに当該イベントの事前条件および事後条件を有するプロパティ群の中から、前記検査対象プログラムの実行により駆動されるイベントの事前条件が真で事後条件が偽となる違反プロパティを、修正対象プロパティとして取得するコンピュータを、
前記検査対象プログラムの全状態遷移列の初期状態から前記修正対象プロパティに該当するイベントの駆動後の状態までの状態遷移列を反例として検出するとともに、前記反例に基づいて、前記初期状態のみまたは当該初期状態から遷移した状態から分岐して到達した末尾の状態に至るイベントにおいて、前記修正対象プロパティの事前条件および事後条件がともに真である状態遷移列を前記反例に対する正例として検出する検出手段、
前記検出手段によって検出された反例および正例の差分となる差分状態遷移列を抽出する差分抽出手段、
前記差分抽出手段によって抽出された差分状態遷移列の中から選ばれたイベントに該当するプロパティの事前条件および事後条件を論理積標準形に変換することにより、変換後の論理式に基づいて差分論理式を抽出する差分論理式抽出手段、
前記差分論理式抽出手段によって抽出された差分論理式の真偽判定を前記正例の最終イベントの駆動元の状態と前記反例の最終イベントの駆動元の状態とにそれぞれおこない、真偽判定結果が前記正例と前記反例とで異なる場合に、前記差分論理式を修正候補となる候補論理式とする生成手段、
前記生成手段によって生成された候補論理式を前記修正対象プロパティの事前条件に追加することにより、修正済プロパティを生成する修正手段、
前記修正手段によって修正された修正済プロパティを出力する出力手段、
として機能させることを特徴とするプロパティ修正プログラム。
【０２２２】
（付記２）前記修正手段は、
前記候補論理式を生成したときの真偽判定結果が前記正例が偽で前記反例が真である場合、前記候補論理式の否定を前記修正対象プロパティの事前条件に追加することにより、修正済プロパティを生成することを特徴とする付記１に記載のプロパティ修正プログラム。
【０２２３】
（付記３）前記検出手段は、
前記正例を複数検出し、
前記差分抽出手段は、
前記複数の正例の中から選ばれた一の正例と前記反例との差分となる差分状態遷移列を抽出し、
前記差分論理式抽出手段は、
前記一の正例と前記反例との差分状態遷移列の中から選ばれたイベントに該当するプロパティの事前条件および事後条件を論理積標準形に変換することにより、変換後の論理式をＯＲ結合した差分論理式を抽出し、
前記生成手段は、
前記差分論理式抽出手段によって抽出された差分論理式の真偽判定を前記複数の正例の最終イベントの駆動元の状態と前記反例の最終イベントの駆動元の状態とにそれぞれおこない、真偽判定結果が前記複数の正例と前記反例とで異なる場合に、前記差分論理式を修正候補となる候補論理式とする付記１に記載のプロパティ修正プログラム。
【０２２４】
（付記４）前記修正手段は、
前記候補論理式を生成したときの真偽判定結果が前記複数の正例が偽で前記反例が真である場合、前記候補論理式の否定を前記修正対象プロパティの事前条件に追加することにより、修正済プロパティを生成することを特徴とする付記３に記載のプロパティ修正プログラム。
【０２２５】
（付記５）前記検出手段は、
前記反例を複数検出するとともに前記正例を複数検出し、
前記差分抽出手段は、
前記複数の正例の中から選ばれた一の正例と前記複数の反例の中から選ばれた一の反例との差分となる差分状態遷移列を抽出し、
前記差分論理式抽出手段は、
前記一の正例と前記一の反例との差分状態遷移列の中から選ばれたイベントに該当するプロパティの事前条件および事後条件を論理積標準形に変換することにより、変換後の論理式に基づいて差分論理式を抽出し、
前記生成手段は、
前記差分論理式抽出手段によって抽出された差分論理式の真偽判定を前記複数の正例の最終イベントの駆動元の状態と前記一の反例の最終イベントの駆動元の状態とにそれぞれおこない、真偽判定結果が前記複数の正例と前記一の反例とで異なる場合に、前記差分論理式を修正候補となる候補論理式とし、
前記修正手段は、
前記候補論理式を前記修正対象プロパティの事前条件に追加し、前記差分抽出手段において未選択の反例がない場合、修正済プロパティとする付記１に記載のプロパティ修正プログラム。
【０２２６】
（付記６）前記修正手段は、
前記候補論理式を生成したときの真偽判定結果が前記複数の正例が偽で前記反例が真である場合、前記候補論理式の否定を前記修正対象プロパティの事前条件に追加することを特徴とする付記５に記載のプロパティ修正プログラム。
【０２２７】
（付記７）前記コンピュータを、
前記差分抽出手段において未選択の正例および未選択の反例がある場合、前記未選択の正例をあらたに前記一の正例として選択するとともに、前記未選択の反例をあらたに前記一の反例として選択する手段として機能させることを特徴とする付記５または６に記載のプロパティ修正プログラム。
【０２２８】
（付記８）検査対象プログラムで駆動されるイベントごとに当該イベントの事前条件および事後条件を有するプロパティ群の中から、前記検査対象プログラムの実行により駆動されるイベントの事前条件が真で事後条件が偽となる違反プロパティを、修正対象プロパティとして取得する検査手段と、
前記検査対象プログラムの全状態遷移列の初期状態から前記修正対象プロパティに該当するイベントの駆動後の状態までの状態遷移列を反例として検出するとともに、前記反例に基づいて、前記初期状態のみまたは当該初期状態から遷移した状態から分岐して到達した末尾の状態に至るイベントにおいて、前記修正対象プロパティの事前条件および事後条件がともに真である状態遷移列を前記反例に対する正例として検出する検出手段と、
前記検出手段によって検出された反例および正例の差分となる差分状態遷移列を抽出する差分抽出手段と、
前記差分抽出手段によって抽出された差分状態遷移列の中から選ばれたイベントに該当するプロパティの事前条件および事後条件を論理積標準形に変換することにより、変換後の論理式に基づいて差分論理式を抽出する差分論理式抽出手段と、
前記差分論理式抽出手段によって抽出された差分論理式の真偽判定を前記正例の最終イベントの駆動元の状態と前記反例の最終イベントの駆動元の状態とにそれぞれおこない、真偽判定結果が前記正例と前記反例とで異なる場合に、前記差分論理式を修正候補となる候補論理式とする生成手段と、
前記生成手段によって生成された候補論理式を前記修正対象プロパティの事前条件に追加することにより、修正済プロパティを生成する修正手段と、
前記修正手段によって修正された修正済プロパティを出力する出力手段と、
を備えることを特徴とするプロパティ修正装置。
【０２２９】
（付記９）検査対象プログラムで駆動されるイベントごとに当該イベントの事前条件および事後条件を有するプロパティ群の中から、前記検査対象プログラムの実行により駆動されるイベントの事前条件が真で事後条件が偽となる違反プロパティを、修正対象プロパティとして取得するコンピュータが、
前記検査対象プログラムの全状態遷移列の初期状態から前記修正対象プロパティに該当するイベントの駆動後の状態までの状態遷移列を反例として検出するとともに、前記反例に基づいて、前記初期状態のみまたは当該初期状態から遷移した状態から分岐して到達した末尾の状態に至るイベントにおいて、前記修正対象プロパティの事前条件および事後条件がともに真である状態遷移列を前記反例に対する正例として検出する検出工程と、
前記検出工程によって検出された反例および正例の差分となる差分状態遷移列を抽出する差分抽出工程と、
前記差分抽出工程によって抽出された差分状態遷移列の中から選ばれたイベントに該当するプロパティの事前条件および事後条件を論理積標準形に変換することにより、変換後の論理式に基づいて差分論理式を抽出する差分論理式抽出工程と、
前記差分論理式抽出工程によって抽出された差分論理式の真偽判定を前記正例の最終イベントの駆動元の状態と前記反例の最終イベントの駆動元の状態とにそれぞれおこない、真偽判定結果が前記正例と前記反例とで異なる場合に、前記差分論理式を修正候補となる候補論理式とする生成工程と、
前記生成工程によって生成された候補論理式を前記修正対象プロパティの事前条件に追加することにより、修正済プロパティを生成する修正工程と、
前記修正工程によって修正された修正済プロパティを出力する出力工程と、
を実行することを特徴とするプロパティ修正方法。
【符号の説明】
【０２３０】
４００  プロパティテーブル
５００  プログラム状態テーブル
６００  プログラム状態遷移テーブル
８００  違反プロパティテーブル
９００  差分論理式テーブル
１０００  候補論理式テーブル
１１００  プロパティ修正装置
１１０１  検査部
１１０２  検出部
１１０３  差分抽出部
１１０４  差分論理式抽出部
１１０５  生成部
１１０６  修正部
１１０７  出力部
２７０１  反例テーブル
２７０２  正例テーブル
２８００  比較済み正例テーブル
【図１】
2010282257.tif 000003
【図２】
2010282257.tif 000004
【図３】
2010282257.tif 000005
【図４】
2010282257.tif 000006
【図５−１】
2010282257.tif 000007
【図５−２】
2010282257.tif 000008
【図５−３】
2010282257.tif 000009
【図５−４】
2010282257.tif 000010
【図５−５】
2010282257.tif 000011
【図５−６】
2010282257.tif 000012
【図５−７】
2010282257.tif 000013
【図５−８】
2010282257.tif 000014
【図５−９】
2010282257.tif 000015
【図５−１０】
2010282257.tif 000016
【図５−１１】
2010282257.tif 000017
【図５−１２】
2010282257.tif 000018
【図５−１３】
2010282257.tif 000019
【図５−１４】
2010282257.tif 000020
【図５−１５】
2010282257.tif 000021
【図５−１６】
2010282257.tif 000022
【図５−１７】
2010282257.tif 000023
【図５−１８】
2010282257.tif 000024
【図５−１９】
2010282257.tif 000025
【図５−２０】
2010282257.tif 000026
【図５−２１】
2010282257.tif 000027
【図６】
2010282257.tif 000028
【図７】
2010282257.tif 000029
【図８】
2010282257.tif 000030
【図９】
2010282257.tif 000031
【図１０】
2010282257.tif 000032
【図１１】
2010282257.tif 000033
【図１２】
2010282257.tif 000034
【図１３】
2010282257.tif 000035
【図１４】
2010282257.tif 000036
【図１５−１】
2010282257.tif 000037
【図１５−２】
2010282257.tif 000038
【図１５−３】
2010282257.tif 000039
【図１６】
2010282257.tif 000040
【図１７】
2010282257.tif 000041
【図１８】
2010282257.tif 000042
【図１９】
2010282257.tif 000043
【図２０】
2010282257.tif 000044
【図２１】
2010282257.tif 000045
【図２２】
2010282257.tif 000046
【図２３】
2010282257.tif 000047
【図２４】
2010282257.tif 000048
【図２５】
2010282257.tif 000049
【図２６】
2010282257.tif 000050
【図２７−１】
2010282257.tif 000051
【図２７−２】
2010282257.tif 000052
【図２８】
2010282257.tif 000053
【図２９】
2010282257.tif 000054
【図３０】
2010282257.tif 000055
【図３１】
2010282257.tif 000056
【図３２−１】
2010282257.tif 000057
【図３２−２】
2010282257.tif 000058
【図３２−３】
2010282257.tif 000059
【図３２−４】
2010282257.tif 000060
【図３２−５】
2010282257.tif 000061
【図３２−６】
2010282257.tif 000062
【図３３】
2010282257.tif 000063
【図３４】
2010282257.tif 000064
【図３５】
2010282257.tif 000065
【図３６】
2010282257.tif 000066
【図３７】
2010282257.tif 000067
【図３８】
2010282257.tif 000068
【図３９】
2010282257.tif 000069
【図４０】
2010282257.tif 000070
【図４１】
2010282257.tif 000071