(57)【特許請求の範囲】
【請求項１】
モデルの状態が遷移する前の入力データの条件を示す事前条件および前記モデルの状態が遷移した後のモデルの状態の条件を変数の関係式で示した事後条件を含むプロパティと、入力データに対して実行される前記モデルの命令文を含む実行トレースとを記憶する記憶部と、
前記実行トレースに含まれる命令文を順方向に辿り、前記プロパティの事前条件に対応する変数を含み結果が真となる条件式を抽出する第１の抽出部と、
前記プロパティの事後条件の関係式に含まれる変数の値の導出に関わった命令文を逆方向から辿り、該関係式を含む命令文を抽出する第２の抽出部と
を備えたことを特徴とするプロパティ分析装置。
【請求項２】
前記第１の抽出部は、前記実行トレースの命令文を順方向に辿る際に、前記プロパティの事前条件の変数の推移関係を表す更新式を基にして推移後の変数を追跡し、追跡中の変数を含む命令文を抽出することを特徴とする請求項１に記載のプロパティ分析装置。
【請求項３】
前記第２の抽出部は、前記実行トレースの命令文を逆方向に辿る際に、前記プロパティの事後条件に含まれる変数の関係式を、該関係式の変数を有する命令文を基にして順次変換し、変換後の関係式の変数を含む命令文を抽出することを特徴とする請求項１または２に記載のプロパティ分析装置。
【請求項４】
前記第２の抽出部が抽出した命令文が実行された場合の値と、該命令文に対応する前記プロパティの事後条件に含まれる変数の関係式から導かれる値とを比較し、比較結果と前記第２の抽出部が抽出した命令文とを対応付ける比較部を更に有することを特徴とする請求項１、２または３に記載のプロパティ分析装置。
【請求項５】
前記比較部による比較の結果、値が一致しない場合には、前記関係式に関連するプロパティを成立させる値を基に、前記第２の抽出部が抽出した命令文の処理前の値を求め、その値を事後条件に含まれる変数の関係式から導かれる値と置き換えて順次比較を行うことを特徴とする請求項４に記載のプロパティ分析装置。
【請求項６】
プロパティ分析装置が、
入力データに対して実行されるモデルの実行トレースに含まれる命令文を順方向に辿り、モデルの状態が遷移する前の入力データの条件を示す事前条件および前記モデルの状態が遷移した後のモデルの状態の条件を変数の関係式で示した事後条件を含むプロパティの前記事前条件に対応する変数を含み結果が真となる条件式を抽出する第１の抽出ステップと、
前記プロパティの事後条件の関係式に含まれる変数の値の導出に関わった命令文を逆方向から辿り、該関係式を含む命令文を抽出する第２の抽出ステップと
を含むことを特徴とするプロパティ分析方法。
【請求項７】
コンピュータに、
入力データに対して実行されるモデルの実行トレースに含まれる命令文を順方向に辿り、モデルの状態が遷移する前の入力データの条件を示す事前条件および前記モデルの状態が遷移した後のモデルの状態の条件を変数の関係式で示した事後条件を含むプロパティの前記事前条件に対応する変数を含み結果が真となる条件式を抽出する第１の抽出手順と、
前記プロパティの事後条件の関係式に含まれる変数の値の導出に関わった命令文を逆方向から辿り、該関係式を含む命令文を抽出する第２の抽出手順と
を実行させることを特徴とするプロパティ分析プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、プロパティ分析装置等に関する。
【背景技術】
【０００２】
ソフトウェアの開発分野では、モデル検査が行われる。検査対象となるモデルは、開発するシステムの挙動や処理内容を記述するものであり、種々のモデルがある。例えば、概要設計の段階では、ＵＭＬ（Unified  Modeling  Language）を用いて、システムが処理する情報の静的構造や処理シーケンスを記述したモデルが利用される。また、システムの開発仕様を厳密に記述する場合には、仕様記述言語を用いて開発仕様をモデルとして記述する。さらに、システムの動的な側面をモデル化する場合には、Promela等のモデル記述用の専用言語を用いて状態遷移等が記述される。また、Java（登録商標）等のプログラム言語で記述されたプログラムも、モデルと見なされる。
【０００３】
ここで、モデル検査で使用されるモデル検査ツールには、様々なものがある。例えば、Promelaで記述されたモデルに対しては、ＳＰＩＮモデルチェッカとよばれるモデル検査ツールがある。また、Javaで記述されたプログラムに対しては、ＪＰＦ（Java  Path  Finder）とよばれるモデル検査ツールがある。
【０００４】
モデル検査ツールの一例として、ＪＰＦについて説明する。このＪＰＦは、Javaプログラムの命令文を、専用のＶＭ（Virtual  Machine）上で順次実行し、命令文の実行によりプログラムの状態が変化した時点で、モデルの仕様を満足するか否かを判定するものである。モデルが仕様として満たすべき性質は、プロパティと呼ばれる。
【０００５】
なお、上記ＪＰＦでは、命令文の実行による全ての状態変化に対して、プロパティが成立しているか否かを逐次判定するものである。このため、ウェブ（Ｗｅｂ）アプリケーションのような大規模プログラムに対してＪＰＦによるモデル検査を実行すると、計算量が膨大なものとなってしまう。このため、現実的には、ＪＰＦは比較的小規模なJavaプログラムに適用することしかできなかった。
【０００６】
これに対して、ウェブアプリケーションのモデル検査を実行する場合に、例えば、画面が遷移したタイミングで、プロパティが成立するか否かを判定するという従来技術が知られている。この従来技術によれば、命令文が実行される度に、プロパティが成立するか否かを判定しなくてもよくなるので、ＪＰＦと比較してモデル検査に要する計算量を削減することができる。
【０００７】
図２７は、ウェブアプリケーションのモデル検査を実行する従来技術を説明するための図である。一例として、ウェブアプリケーションは、画面１ａを表示した後に画面１ａのボタン１ｂが押下されると、プログラム１〜３を実行した後に、画面２ａを表示させるものとする。また、プログラム１〜３にはそれぞれ複数の命令文１１〜１ｍ、２１〜２ｎ、３１〜３ｐが含まれている。上記従来技術では、画面１ａのボタン１ｂが押下され、画面２ａに遷移した時点で、プロパティが成立しているか否かを判定する。このため、従来技術によれば、プログラム１〜３の命令文が実行される毎にプロパティが成立するか否かを判定しないので、計算量を大幅に削減することができる。
【先行技術文献】
【特許文献】
【０００８】
【特許文献１】特開２００９−８７３５２号公報
【特許文献２】特開２００９−８７３５５号公報
【特許文献３】特開平８−０９５８２５号公報
【発明の概要】
【発明が解決しようとする課題】
【０００９】
しかしながら、上記従来技術では、不成立となったプロパティに関連する命令文を正確に特定することができないという問題があった。これは、プロパティの不成立を判定するタイミングと、不成立となったプロパティに関連する命令文が実行されるタイミングとの間に時間的ずれが生じてしまうためである。
【００１０】
図２８は、従来技術の問題点を説明するための図である。図２８の縦軸は時間軸である。ここでは、時間１Ａで前の画面のボタンが押下され、時間２Ａで次の画面が表示される場合について説明する。例えば、前の画面、ボタン、次の画面は、図２７の画面１ａ、ボタン１ｂ、画面２ａに対応する。
【００１１】
従来技術では、次の画面が表示された場合に、プロパティが成立するか否かを判定する。このため、図２８に示すように、従来技術が判定するタイミングは、画面２ａが表示された直後の時間３Ａとなる。これに対して、不成立となったプロパティに関連する命令文は、前の画面から次の画面に遷移する間に存在すると考えられる。ここでは一例として、不成立となったプロパティに関連する命令文が実行された時間を１Ｂとする。そうすると、プロパティの不成立を検出できたとしても、プロパティの不成立を検出した時間と、問題のある命令文が実行された時間は一致せず、時間の開きもある。このため、従来技術の手法を用いても不成立となったプロパティに関連する命令文を正確に特定することはできない。
【００１２】
なお、プロパティの不成立を検出した場合のプログラムを反例トレースとして抽出し、開発者に通知することも行われている。しかし、反例トレースに含まれる命令文には、不成立となったプロパティに関連しない命令文が複数含まれてしまう。このため、不成立となったプロパティに関連する命令文を特定するためには、開発者自身が、反例トレースに含まれる命令文を一つ一つ確認する必要があった。
【００１３】
開示の技術は、上記に鑑みてなされたものであって、不成立となったプロパティに関連する命令文を開発者が容易に特定することができるプロパティ分析装置などを提供することを目的とする。
【課題を解決するための手段】
【００１４】
本願の開示するプロパティ分析装置は、遷移する前のモデルの状態の条件を示す事前条件および前記モデルの状態が遷移した後のモデルの状態の条件を変数の関係式で示した事後条件を含むプロパティを記憶部に記憶する。また、開示のプロパティ分析装置は、ある初期状態において入力データに対して実行される前記モデルの命令文を含む実行トレースを記憶部に記憶する。また、開示のプロパティ分析装置は、前記実行トレースに含まれる命令文を順方向に辿り、前記プロパティの事前条件に対応する変数の推移関係を追跡し、追跡中の変数を含む命令文を抽出する第１の抽出部を備える。また、開示のプロパティ分析装置は、前記プロパティの事後条件の関係式に含まれる変数の値の導出に関わった関係式を逆方向から辿り、該関係式を含む命令文を抽出する第２の抽出部を備える。
【発明の効果】
【００１５】
本願の開示するプロパティ分析装置の一つの態様によれば、不成立となったプロパティに関連する命令文を開発者が容易に特定することができるという効果を奏する。
【図面の簡単な説明】
【００１６】
【図１】図１は、本実施例１にかかるプロパティ分析装置の構成を示す図である。
【図２】図２は、本実施例２にかかるプロパティ分析装置の構成を示す図である。
【図３】図３は、画面遷移モデルを説明するための図である。
【図４Ａ】図４Ａは、検査対象プログラムのソースコードを示す図（１）である。
【図４Ｂ】図４Ｂは、検査対象プログラムのソースコードを示す図（２）である。
【図４Ｃ】図４Ｃは、検査対象プログラムのソースコードを示す図（３）である。
【図５】図５は、プロパティのデータ構造を示す図である。
【図６】図６は、モデル検査部およびプロパティ不成立分析部の構成を示す図である。
【図７】図７は、入力情報のデータ構造を示す図である。
【図８】図８は、プロパティ評価部の処理を説明するための図である。
【図９】図９は、プロパティ不成立テーブルのデータ構造を示す図である。
【図１０】図１０は、実行トレース情報のデータ構造を示す図である。
【図１１】図１１は、事前条件因子テーブルのデータ構造を示す図である。
【図１２】図１２は、パラメータ対応テーブルのデータ構造を示す図である。
【図１３】図１３は、事前条件追跡部が生成する追跡変数リストのデータ構造を示す図である。
【図１４】図１４は、事前条件追跡部の処理を説明するための図である。
【図１５】図１５は、事前結果テーブルのデータ構造を示す図である。
【図１６】図１６は、事前結果テーブルのその他の例を示す図である。
【図１７】図１７は、事後条件因子テーブルのデータ構造を示す図である。
【図１８】図１８は、事後因子条件変換テーブルのデータ構造を示す図である。
【図１９】図１９は、事後条件変換部の処理を説明するための図である。
【図２０】図２０は、関連命令文出力部が表示装置に出力させる表示画面を示す図である。
【図２１】図２１は、本実施例２にかかるプロパティ分析装置の処理手順を示すフローチャートである。
【図２２】図２２は、プロパティ不成立再現部の処理手順を示すフローチャートである。
【図２３】図２３は、実行トレース収集部の処理手順を示すフローチャートである。
【図２４】図２４は、事前条件追跡部の処理手順を示すフローチャートである。
【図２５】図２５は、事後条件変換部の処理手順を示すフローチャートである。
【図２６】図２６は、本実施例にかかるプロパティ分析装置を構成するコンピュータのハードウェア構成を示す図である。
【図２７】図２７は、ウェブアプリケーションのモデル検査を実行する従来技術を説明するための図である。
【図２８】図２８は、従来技術の問題点を説明するための図である。
【発明を実施するための形態】
【００１７】
以下に、本願の開示するプロパティ分析装置の実施例を図面に基づいて詳細に説明する。なお、この実施例によりこの発明が限定されるものではない。
【実施例１】
【００１８】
図１は、本実施例１にかかるプロパティ分析装置１００の構成を示す図である。図１に示すように、このプロパティ分析装置１００は、記憶部１１０、第１の抽出部１２０、第２の抽出部１３０を有する。
【００１９】
記憶部１１０は、プロパティ１１０ａと実行トレース１１０ｂとを記憶する。プロパティ１１０ａは、遷移する前のモデルの状態の条件を示す事前条件およびモデルの状態が遷移した後のモデルの状態の条件を変数の関係式で示した事後条件を含む。実行トレース１１０ｂは、入力データに対して実行されるモデルの命令文を含む。
【００２０】
第１の抽出部１２０は、実行トレース１１０ｂに含まれる命令文を順方向に辿り、プロパティ１１０ａの事前条件に対応する変数の推移関係を追跡し、追跡中の変数を含む命令文を抽出する。
【００２１】
第２の抽出部１３０は、プロパティ１１０ａの事後条件の関係式に含まれる変数の値の導出に関わった関係式を逆方向から辿り、この関係式を含む命令文を抽出する。
【００２２】
プロパティが不成立とは、事前条件が真でかつ事後条件が偽の場合である。よって、プロパティが不成立となる場合には、プロパティの事前条件の変数を利用する条件式が真である条件文の配下の命令文に誤りが存在する可能性がある。このため、プロパティ分析装置１００は、プロパティの事前条件に対応する変数の推移関係を追跡し、追跡中の変数を含む条件文を抽出することで、実行トレース１１０ｂから不成立となったプロパティに関連する条件文を抽出することができる。
【００２３】
また、プロパティが不成立となる場合には、プロパティの事後条件の関係式に含まれる変数の値の導出に関わった命令文に誤りが存在する可能性がある。このため、プロパティ分析装置１００は、事後条件の関係式に含まれる値の導出に関わった命令文を逆方向から辿り、値の導出に係った命令文の関係式を用いて、事後条件の関係式を変換することによって、値の導出に係った命令文の実行時点での事後条件の関係式を算出し、該時点において事後条件の関係式が成立するかどうかを判定することで、値の導出に係った命令文が事後条件の関係式の真偽に与える影響を評価する。これによって、実行トレース１１０ｂから不成立となったプロパティに関連する命令文を抽出することができる。
【００２４】
したがって、プロパティ分析装置１００によれば、プロパティの事前条件が成立してから事後条件が成立するまでの間に複数の命令文が含まれていても、不成立となったプロパティに関連する命令文を開発者が容易に特定することができる。また、プロパティの事後条件が不成立となった時間と、誤りのある命令文が実行された時間との間に時間差がある場合でも、不成立となったプロパティに関連する命令文を開発者が容易に特定することができる。
【実施例２】
【００２５】
図２は、本実施例２にかかるプロパティ分析装置２００の構成を示す図である。図２に示すように、このプロパティ分析装置２００は、記憶部２００ａおよび制御部２００ｂを有し、入力装置３００ａおよび表示装置３００ｂに接続される。入力装置３００ａは、例えば、キーボードやマウスに対応する。表示装置３００ｂは、ディスプレイやモニタ等の表示装置に対応する。
【００２６】
記憶部２００ａは、検査対象プログラム２１０とプロパティ２２０を記憶する。記憶部２００ａは、例えば、ＲＡＭ（Random  Access  Memory）、ＲＯＭ（Read  Only  Memory）、フラッシュメモリ（Flash  Memory）などの半導体メモリ素子、またはハードディスク、光ディスクなどの記憶装置に対応する。
【００２７】
検査対象プログラム２１０は、モデル検査の対象となるプログラムのソースコードである。本実施例２では一例として、検査対象プログラム２１０をウェブアプリケーションのプログラムとする。
【００２８】
プロパティ２２０は、プログラムが仕様として満たすべき性質や条件を示すものである。例えば、プロパティ２２０は、検査対象プログラム２１０が満たすべき性質や条件を論理式で記述したデータとなる。記憶部２００ａが記憶する検査対象プログラム２１０およびプロパティ２２０は、例えば、入力装置３００ａから入力される。
【００２９】
制御部２００ｂは、モデル検査部２３０およびプロパティ不成立分析部２４０を有する。制御部２００ｂは、例えば、ＡＳＩＣ（Application  Specific  Integrated  Circuit）や、ＦＰＧＡ（Field  Programmable  Gate  Array）などの集積装置に対応する。または、制御部２００ｂは、ＣＰＵ（Central  Processing  Unit）やＭＰＵ（Micro  Processing  Unit）等の電子回路に対応する。
【００３０】
モデル検査部２３０は、検査対象プログラム２１０に各種のデータを入力することで、画面遷移モデルの状態遷移を起こさせる。ここで、画面遷移モデルと状態遷移について説明する。
【００３１】
画面遷移モデルとは、ウェブアプリケーションが表示する画面間の遷移関係を記述したものである。例えば、画面遷移モデルは、第１画面でボタンを押下すると第２画面に遷移し、第２画面でボタンを押下すると、第３画面に遷移するといったものである。画面とは、ＨＴＭＬ（HyperText  Markup  Language）等で記述された画面プログラムをウェブブラウザで表示したものである。
【００３２】
この画面遷移モデルに入力される各種のデータは、画面の入力枠に入力される情報と、画面上のボタンが押下されること等とを組み合わせたものに対応する。画面上のボタンが押下される等、検査対象プログラム２１０に対して動作の契機を与えることをイベントと呼ぶ。
【００３３】
状態遷移とは、例えば、所定の変数の値の組が変化することである。例えば、変数Ａの値がａ、変数Ｂの値がｂという状態において、変数Ａの値がａからｃに変化した場合には、状態遷移が起こったことになる。所定の変数の組は、開発者が適宜変更してもよい。
【００３４】
モデル検査部２３０は、検査対象プログラム２１０の各状態において、プロパティ２２０に記述された性質や条件を満足するか否かを判定する。モデル検査部２３０は、プロパティ２２０の不成立を検出した場合に、不成立となったプロパティの情報をプロパティ不成立分析部２４０に通知する。
【００３５】
プロパティ不成立分析部２４０は、モデル検査部２３０から不成立となったプロパティの情報の通知を受けた場合に、モデル検査部２３０と協働して、不成立となったプロパティに関連する命令文を検査対象プログラム２１０から抽出する。そして、プロパティ不成立分析部２４０は、抽出した命令文に関する情報を表示装置３００ｂに出力する。
【００３６】
次に、検査対象プログラム２１０の画面遷移モデルの一例について説明する。図３は、画面遷移モデルを説明するための図である。図３に示すように、この画面遷移モデルは、モデル検査部２３０から入力される各種のデータに応じて、画面を、入力画面１０、商品検索画面１１、金額画面１２または完了画面１３に遷移させる。
【００３７】
入力画面１０は、利用者の氏名、会員種別、購入対象となる商品の名前、商品の単価、商品の数量を入力する画面である。入力画面１０は、氏名枠１０ａ、会員種別枠１０ｂ、商品名枠１０ｃ、単価枠１０ｄ、数量枠１０ｅ、商品検索ボタン１０ｆ、計算ボタン１０ｇを有する。モデル検査部２３０は、氏名枠１０ａおよび会員種別枠１０ｂに氏名と会員種別を入力する。図３に示す例では、氏名枠１０ａに「富士タロウ」が入力され、会員種別枠１０ｂに「ゴールド」が入力される。なお、商品名枠１０ｃ、単価枠１０ｃ、数量１０ｅには、商品検索画面１１での操作に応じた情報が入力される。検査対象プログラム２１０は、入力画面１０の商品検索ボタン１０ｆが押下されるイベントにより、商品検索画面１１に遷移する。また、検査対象プログラム２１０は、入力画面の計算ボタン１０ｇが押下されるイベントにより、金額画面１２に遷移する。
【００３８】
商品検索画面１１は、商品の検索を行う画面である。商品検索画面１１は、商品追加ボタン１１ａを有する。例えば、商品検索画面１１には、商品の一覧、商品の単価、希望する商品の数量が表示される。そして、商品および商品の数量が選択された状態で、商品追加ボタン１１ａが押下されるイベントにより、検査対象プログラム２１０は、入力画面１０に遷移する。そして、検査対象プログラム２１０は、商品検索画面１１で選択された商品の商品名、単価および数量に応じた情報を、入力画面１０の商品名枠１０ｃ、単価枠１０ｄ、数量枠１０ｅに入力する。図３に示す例では、検査対象プログラム２１０は、商品名枠１０ｃに「商品Ａ」を入力し、単価枠１０ｄに「１０００」を入力し、数量１０ｅに「１０」を入力する。なお、モデル検査部２３０が、商品名枠１０ｃ、単価枠１０ｄ、数量枠１０ｅに情報を入力してもよい。
【００３９】
金額画面１２は、商品の合計金額等を表示させて利用者に注文内容を確認させる画面である。金額画面１２は、氏名枠１２ａ、会員種別枠１２ｂ、商品名枠１２ｃ、単価枠１２ｄ、数量枠１２ｅ、割引率枠１２ｆ、割引額枠１２ｇ、金額枠１２ｈを有する。また、金額画面１２は、戻るボタン１２ｉ、購入ボタン１２ｊを有する。このうち、検査対象プログラム２１０は、氏名枠１２ａ、会員種別枠１２ｂ、商品名枠１２ｃ、単価枠１２ｄ、数量枠１２ｅに、入力画面１０の氏名枠１０ａ、会員種別枠１０ｂ、商品名枠１０ｃ、単価枠１０ｄ、数量枠１０ｅに格納された情報を入力する。図３に示す例では、氏名枠１２ａには「富士タロウ」が入力され、会員種別枠１２ｂには「ゴールド」が入力されている。また、商品名枠１２ｃには「商品Ａ」が入力され、単価枠１２ｄには「１０００」が入力され、数量枠１２ｅには「１０」が入力されている。
【００４０】
金額画面１２の割引率枠１２ｆには、割引率が入力される。この割引率は、利用者の会員種別や購入する商品の数量によって算出される値である。検査対象プログラム２１０は、割引率を算出する命令文を実行し、割引率を算出する。検査対象プログラム２１０は、算出した割引率を割引率枠１２ｆに入力する。図３に示す例では、割引率枠１２ｆには「１０％」が入力されている。
【００４１】
金額画面１２の割引額枠１２ｇには、割引率に応じた割引額が入力される。検査対象プログラム２１０は、割引額を算出する命令文を実行し、割引額を算出する。検査対象プログラム２１０は、算出した割引額を割引額枠１２ｇに入力する。図３に示す例では、割引額枠１２ｇには「１０００」が入力されている。
【００４２】
金額画面１２の金額枠１２ｈには、商品の合計金額から割引額を減じた金額が入力される。検査対象プログラム２１０は、金額を算出する命令文を実行し、金額を算出する。検査対象プログラム２１０は、算出した金額を金額枠１２ｈに入力する。図３に示す例では、金額枠１２ｈには「１００００」が入力されている。
【００４３】
また、検査対象プログラム２１０は、金額画面１２の戻るボタン１２ｉが押下されるイベントにより、入力画面１０に遷移する。また、検査対象プログラム２１０は、金額画面１２の購入ボタン１２ｊを押下されるイベントにより、完了画面１３に遷移する。この完了画面１３は、商品の注文が完了した旨を利用者に通知するための画面である。
【００４４】
次に、図３に示した画面遷移モデルを実行する検査対象プログラム２１０のソースコードの一例について説明する。図４Ａ、図４Ｂ、図４Ｃは、検査対象プログラム２１０のソースコードを示す図である。図４Ａ、図４Ｂ、図４Ｃに示すように、この検査対象プログラム２１０は、ソースコード２１０ａ、２１０ｂ、２１０ｃを有する。
【００４５】
このうち、ソースコード２１０ａは、図３に示した画面１０〜１３を表示させる命令文や、割引率、割引額、金額等を算出する命令文を含む。例えば、ソースコード２１０ａの５Ａの命令文は、入力画面１０から入力されたデータを変数に代入するものである。５Ｂの命令文は、ソースコード２１０ｂを利用して割引率を算出するものや、割引額、金額を算出するものである。５Ｃの命令文は、画面１０〜１３を表示させるものである。
【００４６】
ソースコード２１０ｂは、図３に示した入力画面１０の会員種別枠１０ｂに入力されたデータがゴールドか否かに応じて、変数ｎにパラメータ「GOLD」または「NORMAL」を入力するというものである。
【００４７】
ソースコード２１０ｃは、入力画面１０の会員種別枠１０ｂに入力されたデータや、数量枠１０ｅに入力されたデータに応じて、割引率を算出するものである。例えば、５Ｄの命令文は、会員種別が「ノーマル」の場合の割引率を算出するものである。会員種別が「ノーマル」の場合には、割引率の初期値が「０」となり、数量に応じて割引率に値が加算される。具体的には、数量が１０より大きく１００より小さい場合には、割引率に「５％」が加算される。数量が１００より大きい場合には、割引率に「１０％」が加算される。
【００４８】
５Ｅの命令文は、会員種別が「ゴールド」の場合の割引率を算出するものである。会員種別が「ゴールド」の場合には、割引率の初期値が「１５％」となり、数量に応じて割引率に値が加算または減算される。具体的には、数量が１００より大きい場合には、割引率に「５％」が加算される。数量が１０より大きく１００未満の場合には、割引率に「０％」が加算される。数量が１０以下の場合には、割引率から「５％」減算される。
【００４９】
次に、図２に示したプロパティ２２０のデータ構造の一例について説明する。図５は、プロパティ２２０のデータ構造を示す図である。図５に示すように、プロパティ２２０は、プロパティ識別情報およびプロパティ記述を有する。プロパティ識別情報は、プロパティをそれぞれ識別するものである。図５に示す例では、プロパティ２２０には、プロパティ１〜６が含まれる。プロパティ記述は、モデルに要求される仕様や条件を記述したものであり、事前条件と事後条件とからなる。
【００５０】
ここで、事前条件および事後条件について説明する。検査対象プログラム２１０が動作する場合には、動作前の状態が特定の状態であることが想定される。さらに、検査対象プログラム２１０が動作した後に、特定の状態になることが想定される。このように、動作前の状態が特定の状態であることを想定したものを事前条件という。また、動作後の状態が特定の状態になることを想定したものを事後条件という。
【００５１】
図５に示したプロパティ１〜６の事前条件および事後条件の具体的な内容を、図３に示した入力画面１０及び金額画面１２を用いて説明する。まず、プロパティ１の事前条件は、入力画面１０において、会員種別枠１０ｂに「ゴールド」が入力され、かつ、数量枠１０ｅに入力される数値が「１０以上、１００未満」の状態で、計算ボタン１０ｇを押下されることである。プロパティ１の事後条件は、金額画面１２において、割引率枠１２ｆの割引率が「１５％」となることである。
【００５２】
プロパティ２の事前条件は、入力画面１０において、会員種別枠１０ｂに「ゴールド」が入力されず、かつ、数量枠１０ｅに入力される数値が「１０以上、１００未満」の状態で、計算ボタン１０ｇが押下されることである。プロパティ２の事後条件は、金額画面１２において、割引率枠１２ｆの割引率が「５％」となることである。
【００５３】
プロパティ３の事前条件は、入力画面１０において、会員種別枠１０ｂに「ゴールド」が入力され、かつ、数量枠１０ｅに入力される数値が「１００以上」の状態で、計算ボタン１０ｇが押下されることである。プロパティ３の事後条件は、金額画面１２において、割引率枠１２ｆの割引率が「２０％」となることである。
【００５４】
プロパティ４の事前条件は、入力画面１０において、会員種別枠１０ｂに「ゴールド」が入力されず、かつ、数量枠１０ｅに入力される数値が「１００以上」の状態で、計算ボタン１０ｇが押下されることである。プロパティ４の事後条件は、金額画面１２において、割引率枠１２ｆの割引率が「１０％」となることである。
【００５５】
プロパティ５の事前条件は、入力画面１０において、会員種別枠１０ｂに何かしらの会員種別に関するパラメータが入力され、かつ、数量枠１０ｅに入力される数値が「０より大きい」状態で、計算ボタン１０ｇが押下されることである。ここで、会員種別枠１０ｂに入力される会員種別に関するパラメータは、例えば、「ノーマル」または「ゴールド」となる。プロパティ５の事後条件は、金額画面１２において、割引額１２ｇの割引額が、単価枠１２ｄの単価と、数量枠１２ｅの数量と、割引率枠１２ｆの割引率とを乗算した値となることである。
【００５６】
プロパティ６の事前条件は、入力画面１０において、会員種別枠１０ｂに何かしらの会員種別に関するパラメータが入力され、かつ、数量枠１０ｅに入力される数値が「０より大きい」状態で、計算ボタン１０ｇが押下されることである。ここで、会員種別枠１０ｂに入力される会員種別に関するパラメータは、例えば、「ノーマル」または「ゴールド」となる。プロパティ６の事後条件は、金額画面１２において、金額枠１２ｈの金額が、単価枠１２ｄの単価と数量枠１２ｅの数量とを乗算した値から、割引額１２ｇの割引額を減算した値となることである。
【００５７】
次に、図２に示したモデル検査部２３０およびプロパティ不成立分析部２４０の構成を具体的に説明する。図６は、モデル検査部２３０およびプロパティ不成立分析部２４０の構成を示す図である。図６に示すように、モデル検査部２３０は、検査対象プログラム保持部２３１、プロパティ保持部２３２、プログラム駆動部２３３、モデル状態収集部２３４、プロパティ評価部２３５を有する。プロパティ不成立分析部２４０は、プロパティ不成立再現部２４１、実行トレース収集部２４２、事前条件追跡部２４３、事後条件変換部２４４、関連命令文出力部２４５を有する。
【００５８】
検査対象プログラム保持部２３１は、図２に示した記憶部２００ａの検査対象プログラム２１０を取得し、取得した検査対象プログラム２１０を保持する。プロパティ保持部２３２は、記憶部２００ａのプロパティ２２０を取得し、取得したプロパティ２２０を保持する。
【００５９】
プログラム駆動部２３３は、予め設定された入力情報を利用して、検査対象プログラム２１０を網羅的に動作させる処理部である。この入力情報には、画面名や、画面に与えるイベント、画面に入力するパラメータが含まれる。入力情報の具体的な説明は後述する。
【００６０】
モデル情報収集部２３４は、検査対象プログラム２１０の状態が変化する度に、検査対象プログラム２１０の現在の状態を収集する処理部である。このモデル情報収集部２３４が収集する状態には、状態変化が起こった画面の画面名、状態変化が起こった際に画面に与えられたイベント、状態変化が起こった際に画面に入力されたパラメータが含まれる。
【００６１】
プロパティ評価部２３５は、モデル状態収集部２３４が収集した状態と、プロパティ保持部２３２に記憶されたプロパティ２２０とを比較して、プロパティが成立するか否かを判定する処理部である。プロパティ評価部２３５は、プロパティが不成立であると判定した場合には、不成立となったプロパティに関連する情報をプロパティ不成立再現部２４１に通知する。
【００６２】
プロパティ不成立再現部２４１は、不成立となったプロパティに関連するイベントやパラメータを取得する処理部である。まず、プロパティ不成立再現部２４１は、不成立となったプロパティに関連する情報を取得し、検査対象プログラム２１０を再度駆動させる。そして、プロパティ不成立再現部２４１は、検査対象プログラム２１０の駆動を開始した時点の状態からプロパティが不成立となるまでのイベントおよびパラメータの組を取得する。プロパティ不成立再現部２４１は、不成立となったプロパティの識別情報と対応付けて、イベントおよびパラメータの組をプロパティ不成立テーブルに格納する。プロパティ不成立再現部２４１は、プロパティ不成立テーブルを実行トレース収集部２４２に通知する。プロパティ不成立テーブルの具体的な説明は後述する。なお、プロパティ不成立再現部２４１は、不成立となったプロパティに関連するイベントやパラメータを、プログラム駆動部２３３から取得してもよい。
【００６３】
実行トレース収集部２４２は、不成立となったプロパティの事前条件を満たす状態から事後条件に違反する状態までに辿る命令文を、検査対象プログラム２１０から抽出する処理部である。まず、実行トレース収集部２４２は、プロパティ不成立テーブルを利用して、検査対象プログラム２１０を駆動する。実行トレース収集部２４２は、検査対象プログラム２１０に入力するイベントおよびパラメータの組と、不成立となったプロパティとを比較して、不成立となったプロパティの事前条件を満たすか否かを判定する。また、実行トレース収集部２４２は、検査対象プログラム２１０に入力するイベントおよびパラメータの組と、不成立となったプロパティとを比較して、不成立となったプロパティの事後条件を満たすか否かを判定する。そして、実行トレース収集部２４２は、検査対象プログラム２１０から、事前条件が成立した状態から事後条件に違反する状態までに辿る命令文を実行トレース情報として収集する。実行トレース収集部２４２は、実行トレース情報を事前条件追跡部２４３および事後条件変換部２４４に通知する。実行トレース情報の具体的な説明は後述する。
【００６４】
事前条件追跡部２４３は、実行トレース情報を順方向に辿り、不成立となったプロパティの事前条件に関連する命令文を実行トレース情報から取得する処理部である。まず、事前条件追跡部２４３は、不成立となったプロパティの事前条件に対応する変数をプロパティ保持部２３２から取得する。そして、事前条件追跡部２４３は、実行トレース情報を順方向に辿ることで、事前条件に関連する命令文を取得する。事前条件追跡部２４３は、事前条件の変数の推移関係を追跡しながら、実行トレース情報を順方向に辿る。事前条件追跡部２４３の処理の詳細は後述する。
【００６５】
事後条件変換部２４４は、実行トレース情報を逆方向に辿り、プロパティの事後条件に含まれる変数の関係式を、関係式の変数を有する命令文を基にして順次変換し、命令文と変換後の関係式を関連付けて命令文を抽出する処理部である。また、事後条件変換部２４４は、プロパティの事後条件に対応する変数の関係式から導かれる値と、事後条件に対応する命令文を実行した場合の値とを比較し、比較結果を出力する。事後条件変換部２４４の処理の詳細は後述する。
【００６６】
関係命令文出力部２４５は、不成立となったプロパティの事前条件および事後条件に関連する命令文や比較結果等を表示装置３００ｂに出力する処理部である。関係命令文出力部２４５は、不成立となったプロパティの事前条件に関連する命令文を事前条件追跡部２４３から取得する。また、関係命令文出力部２４５は、不成立となったプロパティの事後条件に関連する命令文および比較結果を事後条件変換部２４４から取得する。
【００６７】
次に、プログラム駆動部２３３が利用する入力情報について説明する。図７は、入力情報のデータ構造を示す図である。図７に示すように、この入力情報は、ステップと、画面名と、イベントと、パラメータとを有する。このうち、ステップは、入力順序を示すものである。画面名は、画面を識別するものである。イベントは、画面のボタンを押下するイベントを識別するものである。パラメータは、画面の各枠に入力するパラメータである。画面によっては、入力すべきパラメータが存在しない場合がある。この場合には、パラメータはなしとなる。
【００６８】
図７に示す例では、プログラム駆動部２３３は、ステップ「１」で、検査対象プログラム２１０に「メニュー画面」を表示させ、イベント「買い物」を与える。プログラム駆動部２３３は、ステップ「２」で、検査対象プログラム２１０に「ログイン画面」を表示させる。検査対象プログラム２１０は、「メニュー画面」でイベント「買い物」が与えられると、「ログイン画面」を表示させる。プログラム駆動部２３３は、ログイン画面の所定の枠に「富士タロウ」を入力した後に、イベント「ログイン」を与える。
【００６９】
プログラム駆動部２３３は、ステップ「Ｎ」で、検査対象プログラム２１０に「入力画面」を表示させる。プログラム駆動部２３３は、入力画面の氏名枠に「富士タロウ」、会員種別枠に「ゴールド」、商品名枠に「商品Ａ」、単価枠に「１０００」、数量枠に「１１」を入力した後に、イベント「計算」を与える。このように、プログラム駆動部２３３は、入力情報を利用して、検査対象プログラム２１０を順次駆動させる。
【００７０】
次に、プロパティ評価部２３５の処理を具体的に説明する。プロパティ評価部２３５は、プロパティの事前条件および事後条件を利用して、プロパティが成立するか否かを判定する。まず、プロパティ評価部２３５は、モデル状態収集部２３４から検査対象プログラム２１０の現在の状態を取得し、プロパティ保持部２３２に記憶されたプロパティ２２０と比較することで、プロパティの事前条件を満たすか否かを判定する。
【００７１】
続いて、プロパティ評価部２３５は、プロパティの事前条件を満たすと判定した場合には、該事前条件に対応する事後条件を満たすか否かを判定する。プロパティ評価部２３５は、事後条件を満たすか否かを判定する場合には、事前条件を満たす状態の次に、モデル状態収集部２３４から取得する状態を利用する。
【００７２】
図８は、プロパティ評価部２３５の処理を説明するための図である。入力画面１０において、会員種別枠１０ｂに「ゴールド」が入力され、数量枠１０ｅに「１０」が入力され、計算ボタン１０ｇが押下された場合について説明する。この状態は、プロパティ１，５，６の事前条件を満たす。このため、プロパティ評価部２３５は、入力画面１０から金額画面１２に遷移した後の状態を基にして、プロパティ１，５，６の事後条件を満たすか否かを判定する。
【００７３】
プロパティ１の事後条件は、図８の３Ａに示すように、割引率枠１２ｆの割引率が「１５％」になるというものである。図８では、金額画面１２において、割引率枠１２ｆの割引率が「１０％」となっている。プロパティ１の事後条件を満たさないため、プロパティ評価部２３５は、プロパティ１が不成立であると判定する。
【００７４】
プロパティ５の事後条件は、図８の３Ｂに示すように、割引額枠１２ｇの割引額が、単価枠１２ｄの値と、数量枠１２ｅの値と、割引率枠１２ｆの割引率とを乗算した値と等しくなるというものである。図８において、単価枠１２ｄの値「１０００」と、数量枠１２ｅの値「１０」と、割引率枠１２ｆの割引率「１０％」とを乗算した値は「１０００」となる。このため、各値を乗算した値は割引額枠１２ｇの割引額と等しくなり、プロパティ評価部２３５は、プロパティ５が成立すると判定する。
【００７５】
プロパティ６の事後条件は、図８の３Ｃに示すように、金額枠１２ｈの金額が、単価枠１２ｄの値と、数量枠１２ｅの値との乗算結果から、割引額枠１２ｇの割引額を減算した値と等しくなるというものである。図８において、単価枠１２ｄの値「１０００」と、数量枠１２ｅの値「１０」との乗算結果「１００００」から、割引額枠１２ｇの割引額「１０００」を減算すると「９０００」となる。これに対して、演算結果が金額枠１２ｈの金額は「１００００」なる。各値が異なるので、プロパティ評価部２３５は、プロパティ６が不成立であると判定する。
【００７６】
次に、プロパティ不成立再現部２４１が保持するプロパティ不成立テーブルについて説明する。図９は、プロパティ不成立テーブルのデータ構造を示す図である。図９に示すように、このプロパティ不成立テーブルは、不成立プロパティ識別情報と、ステップと、画面名と、イベントと、パラメータとを有する。このうち、不成立プロパティ識別情報は、不成立となったプロパティを識別するものである。ステップ、画面名、イベント、パラメータに関する説明は、図７に示したステップ、画面名、イベント、パラメータに関する説明と同様である。
【００７７】
図９に示すように、検査対象プログラム２１０が表示する画面のうち、画面名「メニュー」に対応する画面から、画面名「入力画面」に対応する画面に遷移するまでに入力されたイベントおよびパラメータが対応付けられている。図９に示す例では、入力画面の氏名枠に「富士タロウ」、会員種別枠に「ゴールド」、商品名枠に「商品Ａ」、単価枠に「１０００」、数量枠に「１０」を入力した後に、イベント「計算」を与えた場合に、プロパティ１、６が不成立となったことを意味する。
【００７８】
次に、実行トレース収集部２４２が収集する実行トレース情報の一例について説明する。図１０は、実行トレース情報のデータ構造を示す図である。図１０に示す例では、実行トレース情報は、プロパティ１およびプロパティ６の事前条件が成立し、事後条件が不成立となるまでに辿った検査対象プログラム２１０の命令文を有する。
【００７９】
この実行トレース情報には、ナンバ（Ｎｏ）、プログラム識別情報、ライン（ｌｉｎｅ）、実行トレース、変数値が含まれる。ナンバは、命令文の収集順序を示すものである。プログラム識別情報は、命令文を収集したプログラムを識別するものである。例えば、プログラム識別情報「Servlet」は、図４Ａに示したプログラム２１０ａに対応する。プログラム識別情報「CustmerRank」は、図４Ｂに示したプログラム２１０ｂに対応する。プログラム識別情報「DiscountRate」は、図４Ｃに示したプログラム２１０ｃに対応する。ラインは、該当する命令文が存在するプログラム上の行を識別するものである。実行トレースは、命令文に対応する。変数値は、命令文に含まれる変数と、命令文が実行された後に該命令文の変数に入力される値との関係を示すものである。なお、命令文が条件式の場合には、変数値には、「TRUE」または「FALSE」が入力される。条件式を満たす場合には、条件式に対応する変数値は「TRUE」となる。条件式を満たさない場合には、条件式に対応する変数値は「FALSE」となる。
【００８０】
ここで、図１０のナンバ「１〜２９」の命令文の概要について説明する。ナンバ「１〜４」の命令文は、図８の入力画面１０にて入力されたパラメータを変数に代入するものである。ナンバ「１」の命令文は、入力画面１０の会員種別枠１０ｂに入力された値を変数rankに入力するものである。変数rankには、「ゴールド」が入力される。ナンバ「２」の命令文は、入力画面１０の単価枠１０ｄに入力された値を変数unitpriceに入力するものである。変数unitpriceには、「１０００」が入力される。ナンバ「３」の命令文は、入力画面１０の数量枠１０ｅに入力された値を変数amountに入力するものである。変数amountには「１０」が入力される。ナンバ「４」の命令文は、変数discountの初期値を設定するものである。変数discountには、「０」が初期値として入力される。
【００８１】
ナンバ「５〜１１」の命令文は、変数rankの値が「ゴールド」の場合に、変数rankCodeに「CODE-G」を入力するものである。ナンバ「５」の説明は省略する。ナンバ「６」の変数ｎには、変数rankの値「ゴールド」が入力される。ナンバ「７」の変数codeには、「空」が入力される。ナンバ「８」の命令文は変数ｎの値がゴールドであるか否かを判定する条件式である。ここでは、変数ｎの値が「ゴールド」であるため、条件式を満たす。このため、ナンバ「８」の変数値は、「TRUE」となる。ナンバ「９」の変数codeには、「CODE-G」が入力される。ナンバ「１０」の命令文でcodeの値が返されることで、ナンバ「１１」の変数rankCodeには、「CODE-G」が入力される。
【００８２】
ナンバ「１２〜１３」の命令文は、入力された値を整数として、変数に入力するものである。ナンバ「１２」の命令文は、変数unitpriceの値を整数として変数tankaに入力するものである。変数tankaには、「１０００」が入力される。ナンバ「１３」の命令文は、変数amountの値を整数として変数suryoに入力するものである。変数suryoには、「１０」が入力される。
【００８３】
ナンバ「１４〜２６」の命令文は、変数cおよび変数numの値に応じて値を算出し、算出した値を変数rateに入力するものである。ここで、変数cは会員種別に対応し、変数numは数量に対応し、変数rateは割引率に対応する。ナンバ「１４」の説明は省略する。
【００８４】
ナンバ「１５」の変数cには「CODE-G」が入力され、変数numには「１０」が入力される。ナンバ「１６」は変数rateのインスタンスを定義するものである。ナンバ「１７」の命令文は、変数cの値と「CustmerRank.NORMAL」の値とが等しいか否かを判定する条件式である。ここで、変数cの値が「CODE-G」であり、「CustmerRank.NORMAL」の値が「CODE-N」である。このため、ナンバ「１７」の条件式を満たさず、ナンバ「１７」の変数値は「FALSE」となる。
【００８５】
ナンバ「１８」の命令文は、変数cの値と「CustmerRank.GOLD」の値とが等しいか否かを判定する条件式である。ここで、変数cの値が「CODE-G」であり、「CustmerRank.GOLD」の値が「CODE-G」である。このため、条件式を満たすため、ナンバ「１８」の変数値は「TRUE」となる。
【００８６】
ナンバ「１９」の命令文は、変数aaの値が１と等しいか否かを判定する条件式である。ここで、変数aaの初期値は「１」であり、条件式「aa=１」を満たす。このため、ナンバ「１９」の変数値は、「TRUE」となる。ナンバ「２０」の命令文では、変数rateに「０．１５」が入力される。
【００８７】
ナンバ「２１」の命令文は、変数numの値が１００より大きいか否かを判定する条件式である。ここでは、変数numの値が「１０」であるため、条件式「num＞１００」を満たさない。このため、ナンバ「２１」の変数値は「FALSE」となる。
【００８８】
ナンバ「２２」の命令文は、変数numの値が１０より大きいか否かを判定する条件式である。ここでは、変数numの値が「１０」であるため条件式「num>１０」を満たさない。このため、ナンバ「２２」の変数値は「FALSE」となる。
【００８９】
ナンバ「２３」の命令文は、変数numの値が１００以下であるか、または、変数numの値が１０以下であるかを判定する条件式である。ここでは、変数numの値が「１０」であるため条件式「num<=１００  or  num<=１０」を満たす。このため、ナンバ「２３」の変数値は「TRUE」となる。
【００９０】
ナンバ「２４」の命令文は、変数rateの現在の値から「０．０５」を減算し、減算結果を変数rateに入力するものである。ナンバ「２５」の命令文でrateが返されることで、ナンバ「２６」の変数rateには「０．１０」が入力される。
【００９１】
ナンバ「２７〜２９」の命令文は、割引率、割引額、金額の値を算出し、算出した値をそれぞれ変数rateParcent、変数discount、変数totalに入力するものである。ナンバ「２７」の命令文は、変数rateの値に１００を乗算した結果を、変数rateParcentに入力するものである。変数rateParcentには、「１０」が入力される。ナンバ「２８」の命令文は、変数tankaの値と変数suryoの値とを乗算した結果から、変数discountの値を減算した値を、変数totalに入力するものである。変数totalには、「１００００」が入力される。ナンバ「２９」の命令文は、変数totalの値と変数rateの値とを乗算した結果を、変数discountに入力するものである。変数discountには、「１０００」が入力される。
【００９２】
ナンバ「２７」の変数rateParcentに入力された値「１０」が「％」を付加された状態で、図８の金額画面１２の割引率枠１２ｆに入力される。ナンバ「２８」の変数totalに入力された値「１００００」が、図８の金額画面１２の金額枠１２ｈに入力される。ナンバ「２９」の変数discountに入力された値「１０００」が、図８の金額画面１２の割引額枠１２ｇに入力される。
【００９３】
次に、事前条件追跡部２４３の処理を具体的に説明する。まず、事前条件追跡部２４３は、不成立となったプロパティの事前条件をプロパティ保持部２３２から抽出し、事前条件から事前条件因子テーブルを生成する。ここでは、不成立となったプロパティをプロパティ１，６とする。
【００９４】
事前条件追跡部２４３が生成する事前条件因子テーブルのデータ構造の一例について説明する。図１１は、事前条件因子テーブルのデータ構造を示す図である。図１１に示すように、この事前条件因子テーブルは、プロパティ識別情報、ＩＤ（Identification）、事前条件の因子条件、画面、項目、因子間の関係を有する。
【００９５】
プロパティ識別情報は、プロパティを識別するものである。ＩＤは、プロパティに含まれる事前条件の因子条件を識別するものである。事前条件の因子条件は、事前条件をなす因子条件である。プロパティ１の事前条件の因子条件は、「入力画面．会員種別＝“ゴールド”」、「入力画面．数量＞＝１０」、「入力画面．数量＜１００」である。プロパティ６の事前条件の因子条件は、「入力画面．会員種別！＝“”」、「入力画面．数量＞０」である。
【００９６】
画面は、事前条件の因子条件に対応する画面名を示すものである。事前条件の因子条件「入力画面．会員種別＝“ゴールド”」に対応する画面は、入力画面である。事前条件の因子条件「入力画面．数量＞＝１０」に対応する画面は、入力画面である。事前条件の因子条件「入力画面．数量＜１００」に対応する画面は、入力画面である。事前条件の因子条件「入力画面．会員種別！＝“”」に対応する画面は、入力画面である。事前条件の因子条件「入力画面．数量＞０」に対応する画面は、入力画面である。
【００９７】
項目は、事前条件の因子条件に対応する画面の項目を示すものである。事前条件の因子条件「入力画面．会員種別＝“ゴールド”」に対応する項目は、入力画面の会員種別に対応する。事前条件の因子条件「入力画面．数量＞＝１０」に対応する項目は、入力画面の数量に対応する。事前条件の因子条件「入力画面．数量＜１００」に対応する項目は、入力画面の数量に対応する。事前条件の因子条件「入力画面．会員種別！＝“”」に対応する項目は、入力画面の会員種別に対応する。事前条件の因子条件「入力画面．数量＞０」に対応する項目は、入力画面の数量に対応する。
【００９８】
因子間の関係は、事前条件の各因子条件の関係を示すものである。各因子条件の関係には、包含関係、両立等の関係がある。例えば、因子条件Ａが因子条件Ｂを包含する場合には、因子条件Ａと因子条件Ｂとの関係が包含関係であり、因子条件Ｂは因子条件Ａよりも条件が厳しい。因子条件Ａと因子条件Ｂが両立する場合には、因子条件Ａの条件と因子条件Ｂの条件とが同時に成り立つ場合があることを示す。
【００９９】
図１１に示すように、ＩＤ「P6_pre1」の因子条件はＩＤ「P1_pre1」の因子条件を包含する。ＩＤ「P6_pre2」の因子条件はＩＤ「P1_pre2」の因子条件を包含する。ＩＤ「P1_pre2」の因子条件とＩＤ「P1_pre3」の因子条件は両立する。ＩＤ「P1_pre3」の因子条件とＩＤ「P1_pre2」の因子条件は両立する。ＩＤ「P1_pre3」の因子条件とＩＤ「P6_pre2」の因子条件は両立する。因子間の関係は、予め設定されているものとする。
【０１００】
事前条件追跡部２４３は、上記事前条件因子テーブルを生成した後に、事前条件因子テーブルに含まれる事前条件の因子条件を、プログラム変数に変換する。このプログラム変数は、検査対象プログラム２１０の変数に対応する。事前条件追跡部２４３は、パラメータ対応テーブルと事前条件因子テーブルとを比較することで、事前条件の因子条件をプログラム変数に変換する。このパラメータ対応テーブルは、事前条件の因子条件に対応する画面および項目の組と、プログラム変数とを対応付けたものである。事前条件追跡部２４３は、事後条件の因子条件をプログラム変数に変換したものを、追跡変換リストに登録する。ここで、パラメータ対応テーブルのデータ構造の一例について説明する。
【０１０１】
図１２は、パラメータ対応テーブルのデータ構造を示す図である。図１２に示すように、このパラメータ対応テーブルは、ナンバ（Ｎｏ）、画面、項目、プログラム変数を有する。ナンバは、画面と項目とプログラム変数との組を識別するものである。画面は、画面を識別するものであり、項目は画面上の項目を識別するものである。プログラム変数は、検査対象プログラム２１０で利用される変数である。
【０１０２】
事前条件追跡部２４３は、パラメータ対応テーブルの画面および項目の組と、事前条件因子テーブルの画面および項目の組とを比較して、プログラム変数を特定する。例えば、事前条件の因子条件「入力画面．会員種別」は、パラメータ対応テーブルのナンバ「１」の画面「入力画面」および項目「会員種別」の組に対応する。このため、事前条件追跡部２４３は、事前条件の因子条件「入力画面．会員種別＝“ゴールド”」をプログラム変数「custmer」に変換する。
【０１０３】
ここで、事前条件追跡部２４３が、図１１の事前条件因子テーブルから生成する追跡変数リストについて説明する。図１３は、事前条件追跡部２４３が生成する追跡変数リストのデータ構造を示す図である。図１３に示すように、この追跡変数リストは、変数「custmer」、「amount」を有する。なお、事前条件追跡部２４３は、追跡変数リストの変数のうち、重複する変数を一つの変数にまとめるものとする。
【０１０４】
事前条件追跡部２４３は、追跡変数リストを生成した後に、実行トレース情報を順方向に辿りながら、追跡変数リストの変数の推移関係を追跡する。事前条件追跡部２４３は、命令文を参照し、該命令文が更新式であり、かつ、更新式の右辺に追跡変数リストの変数が含まれている場合に、更新式の左辺の変数を追跡変数リストに追加することで、変数の推移関係を追跡する。
【０１０５】
そして、事前条件追跡部２４３は、追跡変数リストの変数を処理する「条件式」であり、かつ、該条件式の変数値が「TRUE」となる命令文を、不成立となったプロパティの事前条件に関連する命令文として特定する。事前条件追跡部２４３は、事前条件に関連する命令文を、事前条件関連文リストに追加する。
【０１０６】
なお、事前条件追跡部２４３は、変数を追跡変数リストに追加する場合には、更新方法の値付きで、追跡変数リストに追加する。更新方法の値には、取得、転記、変換が含まれる。ここで、更新方法が取得とは、更新後の変数に入力された値が、外部から取得したデータに対応することを意味する。更新方法が転記とは、更新後の変数に入力された値が、転記された値であることを示す。更新方法が変換とは、更新後の変数に入力された値が、変換された値であることを示す。
【０１０７】
図１４は、事前条件追跡部２４３の処理を説明するための図である。図１４では、ナンバ（Ｎｏ）、プログラム識別情報、ライン（ｌｉｎｅ）、実行トレース、変数値、追跡変数リスト、事前条件関連を用いて事前条件追跡部２４３の処理を説明する。このうち、ナンバ、プログラム識別情報、ライン、実行トレース、変数値は、図１０に示したナンバ、プログラム識別情報、ライン、実行トレース、変数値と同様である。
【０１０８】
また、図１４において、追跡変数リストは、図１３に示した追跡変数リストに含まれる変数を示す。ただし、初期の段階で追跡変数リストに含まれる変数「custmer」、「amount」の記載は省略する。事前条件関連は、該当する命令文が条件式の場合に、この条件式の利用する変数が直接的な変数であるか間接的な変数であるかを示すものである。ここで、直接的な変数とは、プログラムが内部的に処理していない変数である。間接的な変数とは、プログラムが内部的に処理した変数である。直接的な変数を用いる条件式に対応する事前条件関連は「直接」となる。これに対して、間接的な変数を用いる条件式に対応する事前条件関連は「間接」となる。
【０１０９】
なお、ここでは説明の便宜上、事前条件追跡部２４３は、実行トレースの先頭が「＞」となる命令文をスキップする。
【０１１０】
図１４のナンバ「１」の命令文は更新式であり、この更新式の右辺には、追跡変数リストの変数「custmer」が含まれている。このため、事前条件追跡部２４３は、ナンバ「１」の命令文の左辺の変数「rank」を追跡変数リストに追加する。変数「rank」の更新方法の値は「取得」となる。
【０１１１】
ナンバ「２」の命令文は更新式であるが、該命令文の右辺に追跡変数リストの変数が含まれていない。このため、事前条件追跡部２４３は、ナンバ「２」の命令文に対する処理を終了する。ナンバ「３」の命令文は更新式であり、この更新式の右辺に追跡変数リストの変数「amount」が含まれている。このため、事前条件追跡部２４３は、ナンバ「３」の命令文の左辺の変数「amount」を追跡変数リストに追加する。変数「amount」の更新方法の値は「取得」となる。
【０１１２】
ナンバ「４」、「５」の命令文は、追跡変数リストの変数を含んでいない。このため、事前条件追跡部２４３は、ナンバ「４」、「５」の命令文に対する処理を終了する。ナンバ「６」の命令文は、変数「rank」をプログラム２１０ｂで「n」として利用する旨を示す。変数「rank」は、追跡変数リストに含まれている。この場合には、事前条件追跡部２４３は、変数「n」を追跡変数リストに追加する。変数「n」の更新方法の値は「転記」となる。
【０１１３】
ナンバ「７」の命令文は更新式であるが、この更新式の右辺に追跡変数リストの変数が含まれていない。このため、事前条件追跡部２４３は、ナンバ「７」の命令文に対する処理を終了する。
【０１１４】
ナンバ「８」の命令文は条件式であり、この条件式は追跡変数リストの変数「n」を含んでいる。また、この条件式に対応する変数値は「TRUE」である。このため、事前条件追跡部２４３は、ナンバ「８」の命令文を、不成立となったプロパティの事前条件に関連する命令文として特定する。具体的には、命令文は「n.equals(“ゴールド”)」となる。なお、ナンバ「８」の命令文は、入力画面から入力された値「ゴールド」を直接利用する条件式である。このため、事前条件追跡部２４３は、ナンバ「８」の命令文の事前条件関連を「直接」に設定する。事前条件追跡部２４３は、ナンバ「８」の命令文に関する情報を、事前条件関連文リストに追加する。
【０１１５】
ナンバ「９」、「１０」の命令文は、追跡変数リストの変数を含んでいない。このため、事前条件追跡部２４３は、ナンバ「９」、「１０」の命令文に対する処理を終了する。ナンバ「１１」の命令文は、更新式であり、この更新式の右辺に追跡変数リストの変数「rank」が含まれている。このため、事前条件追跡部２４３は、ナンバ「１１」の命令文の左辺の変数「rankCode」を追跡変数リストに追加する。変数「rankCode」の更新方法の値は「変換」となる。
【０１１６】
ナンバ「１２」の命令文は更新式であるが、この更新式の右辺に追跡変数リストの変数が含まれていない。このため、事前条件追跡部２４３は、ナンバ「１２」の命令文に対する処理を終了する。ナンバ「１３」の命令文は更新式であり、該更新式の右辺に追跡変数リストの変数「amount」が含まれている。このため、事前条件追跡部２４３は、ナンバ「１３」の左辺の変数「suryo」を追跡変数リストに追加する。変数「suryo」の更新方法の値は「変換」となる。
【０１１７】
事前条件追跡部２４３は、ナンバ「１４」の命令文の先頭が「＞」であるため、ナンバ「１４」の命令文に対する処理を終了する。ナンバ「１５」の命令文は、変数「rankCode」の値をプログラム２１０ｃで変数「c」の値として利用し、変数「suryo」の値をプログラム２１０ｃで「num」の値として使用する旨を示す。変数「rankCode」、変数「suryo」は、追跡変換リストに含まれている。この場合には、事前条件追跡部２４３は、変数「c」および変数「num」を追跡変数リストに追加する。変数「c」の更新方法の値は「変換」、変数「num」の更新方法の値は「転記」となる。
【０１１８】
ナンバ「１６」の命令文は、変数「rate」のインスタンスを生成する命令文であるため、条件式、更新式に該当しない。このため、事前条件追跡部２４３は、ナンバ「１６」の命令文に対する処理を終了する。
【０１１９】
ナンバ「１７」の命令文は条件式であり、この条件式は追跡変数リストの変数「c」を含んでいる。しかし、この条件式に対応する変数値は「FALSE」である。このため、事前条件追跡部２４３は、ナンバ「１７」の命令文を、不成立となったプロパティの事前条件に関連する命令文として特定しない。ナンバ「１７」の命令文は、内部的に処理した変数の値「CODE-G」を利用する条件式である。このため、事前条件追跡部２４３は、ナンバ「１７」の命令文の事前条件関連を「間接」に設定する。
【０１２０】
ナンバ「１８」の命令文は条件式であり、この条件式は追跡変数リストの変数「c」を含んでいる。また、この条件式に対応する変数値は「TRUE」である。このため、事前条件追跡部２４３は、ナンバ「１８」の命令文を、不成立となったプロパティの事前条件に関連する命令文として特定する。具体的には、命令文は「c.equals(CustmerRank.GOLD)」となる。また、ナンバ「１８」の命令文は、内部的に処理した変数の値「CODE-G」を利用する条件式である。このため、事前条件追跡部２４３は、ナンバ「１８」の命令文の事前条件関連を「間接」に設定する。事前条件追跡部２４３は、ナンバ「１８」の命令文に関する情報を、事前条件関連文リストに追加する。
【０１２１】
ナンバ「１９」の命令文は条件式であるが、この条件式には追加変数リストの変数が含まれていない。このため、事前条件追跡部２４３は、ナンバ「１９」の命令文に対する処理を終了する。
【０１２２】
ナンバ「２０」の命令文は更新式であるが、この命令文の右辺に追跡変数リストの変数が含まれていない。このため、事前条件追跡部２４３は、ナンバ「２０」の命令文に対する処理を終了する。
【０１２３】
ナンバ「２１」の命令文は条件式であり、この条件式は追跡変数リストの変数「num」を含んでいる。しかし、この条件式に対応する変数値は「FALSE」である。このため、事前条件追跡部２４３は、ナンバ「２１」の命令文を、不成立となったプロパティの事前条件に関連する命令文として特定しない。ナンバ「２１」の命令文は、入力画面から入力された値「１０」を直接利用する条件式である。このため、事前条件追跡部２４３は、ナンバ「２１」の命令文の事前条件関連を「直接」に設定する。
【０１２４】
ナンバ「２２」の命令文は条件式であり、この条件式は追跡変数リストの変数「num」を含んでいる。しかし、この条件式に対応する変数値は「FALSE」である。このため、事前条件追跡部２４３は、ナンバ「２２」の命令文を、不成立となったプロパティの事前条件に関連する命令文として特定しない。ナンバ「２２」の命令文は、入力画面から入力された値「１０」を直接利用する条件式である。このため、事前条件追跡部２４３は、ナンバ「２２」の命令文の事前条件関連を「直接」に設定する。
【０１２５】
ナンバ「２３」の命令文は条件式であり、この条件式は追跡変数リストの変数「num」を含んでいる。また、この条件式に対応する変数値は「TRUE」である。このため、事前条件追跡部２４３は、ナンバ「２３」の命令文を、不成立となったプロパティの事前条件に関連する命令文として特定する。具体的には、命令文は「num<=100  or  num<=10」となる。なお、ナンバ「２３」の命令文は、入力画面から入力された値「１０」を直接利用する条件式である。このため、事前条件追跡部２４３は、ナンバ「２３」の命令文の事前条件関連を「直接」に設定する。事前条件追跡部２４３は、ナンバ「２３」の命令文に関する情報を、事前条件関連文リストに追加する。
【０１２６】
ナンバ「２４」の命令文は更新式であるが、この更新式の右辺に追跡変数リストの変数が含まれていない。このため、事前条件追跡部２４３は、ナンバ「２４」の命令文に対する処理を終了する。ナンバ「２５」の命令文は条件式ではなく、更新式でもない。このため、事前条件追跡部２４３は、ナンバ「２５」の命令文に対する処理を終了する。
【０１２７】
ナンバ「２６」の命令文は更新式であり、この更新式の右辺に追加変数リストの変数「rankCode」および変数「suryo」が含まれている。このため、事前条件追跡部２４３は、ナンバ「２６」の命令文の左辺の変数「rate」を追跡変数リストに追加する。変数「rate」の更新方法の値は「変換」となる。
【０１２８】
ナンバ「２７」の命令文は更新式であり、この更新式の右辺に追跡変数リストの変数「rate」が含まれている。このため、事前条件追跡部２４３は、ナンバ「２７」の命令文の左辺の変数「ratePercent」を追跡変数リストに追加する。変数「ratePercent」の更新方法の値は「変換」となる。
【０１２９】
ナンバ「２８」の命令文は更新式であり、この更新式の右辺に追跡変数リストの変数「suryo」が含まれている。このため、事前条件追跡部２４３は、ナンバ「２８」の命令文の左辺の変数「total」を追跡変数リストに追加する。変数「total」の更新方法の値は「変換」となる。
【０１３０】
ナンバ「２９」の命令文は更新式であり、この更新式の右辺に追跡変数リストの変数「total」および変数「rate」が含まれている。このため、事前条件追跡部２４３は、ナンバ「２９」の左辺の変数「discount」を追跡変数リストに追加する。変数「discount」の更新方法の値は「変換」となる。
【０１３１】
上記のように事前条件追跡部２４３は、ナンバ「１」〜「２９」の命令文を順方向に辿ることで、事前条件に関連する命令文を事前条件関連文リストに追加する。事前条件追跡部２４３は、事前条件関連文リストと事前条件因子テーブルとを基にして、事前結果テーブルを生成する。
【０１３２】
なお、事前条件追跡部２４３は、追加変数リストに追加した変数のうち、今後利用しない変数を、スコープから外れた変数として追跡変数リストから削除してもよい。例えば、事前条件追跡部２４３は、ナンバ「２５」の命令文に対する処理が終了した後に、追跡変数リストから変数「c」、「num」をスコープから外れた変数と判定する。事前条件追跡部２４３は、ナンバ「２５」の命令文に対する処理が終了した後に、追跡変数リストから変数「c」、「num」を削除する。
【０１３３】
次に、事前結果テーブルのデータ構造の一例について説明する。図１５は、事前結果テーブルのデータ構造を示す図である。図１５に示すように、この事前結果テーブルは、ナンバ（Ｎｏ）と、事前条件の関連条件文と、プログラム識別情報と、ライン（ｌｉｎｅ）と、変数と、事前条件関連と、因子条件項目と、関連する因子条件とを有する。ナンバは、条件式の収集順序を示すものである。事前条件の関連条件文は、事前条件に関連する命令文を示すものである。プログラム識別情報は、該当する命令文を有するプログラムを示すものである。ラインは、該当する命令文が存在する行である。変数は、該当する命令文に含まれる変数である。事前条件関連は、図１４に示した事前条件関連に対応するものである。
【０１３４】
図１５の因子条件項目は、事前条件に関連する命令文の変数に対応する項目である。関連する因子条件は、該当する命令文に対応するＩＤである。例えば、事前条件追跡部２４３は、事前結果テーブルの因子条件項目と、図１１に示した事前条件因子テーブルとを比較して、関連する因子条件を特定する。
【０１３５】
図１５において、ナンバ「１」に対応する事前条件の関連条件文は「（n.equals(“ゴールド”)）」となる。ナンバ「１」に対応するその他の情報は、プログラム識別情報「CustmerRank」、ライン「９」、変数「ｎ」、事前条件関連「直接」、因子条件項目「入力画面．会員種別」、関連する因子条件「P1_pre1,P6_pre1」となる。
【０１３６】
ナンバ「２」に対応する事前条件の関連条件文は「（c.equals(CustmerRank.GOLD)」となる。ナンバ「２」に対応するその他の情報は、プログラム識別情報「DiscountRate」、ライン「２３」、変数「ｃ」、事前条件関連「間接」、因子条件項目「入力画面．会員種別」、関連する因子条件「P1_pre1,P6_pre1」となる。ナンバ「３」に対応する事前条件の関連条件文は「num<=10  or  num<=100」となる。ナンバ「３」に対応するその他の情報は、プログラム識別情報「DiscountRate」、ライン「３０」、変数「num」、事前条件関連「直接」、因子条件項目「入力画面．数量」、関連する因子条件「P1_pre2,P1_pre3,P6_pre2」となる。
【０１３７】
なお、事前条件追跡部２４３が生成する事前結果テーブルは、図１５のものに限られない。図１６は、事前結果テーブルのその他の例を示す図である。図１６に示すように、この事前結果テーブルは、プロパティ識別情報と、ＩＤと、事前条件の因子条件と、事前条件の関連条件文と、事前条件関連と、プログラム識別情報と、ライン（ｌｉｎｅ）を有する。このうち、プロパティ識別情報、ＩＤ、事前条件の因子条件は、図１１で説明したプロパティ識別情報、ＩＤ、事前条件の因子条件と同様である。また、事前条件の関連条件文、事前条件関連、プログラム識別情報、ラインは、図１５に示した事前条件の関連条件文、事前条件関連、プログラム識別情報、ラインと同様である。なお、ＩＤ「P6_pre1」に対応する事前条件の関連条件文は、「P6_pre1⊃P1_pre1」となっている。これは、ＩＤ「P6_pre1」に対応する事前条件の関連条件文が、ＩＤ「P1_pre1」に対応する事前条件の関連条件文を含んでいることを示す。事前条件追跡部２４３は、図１５に示した事前結果テーブルまたは図１６に示した事前結果テーブルどちらかを生成してもよいし、両方とも作成してもよい。
【０１３８】
図１６において、プロパティ識別情報には「プロパティ１」、「プロパティ６」が含まれる。また、ＩＤには「P1_pre1」、「P1_pre2」、「P1_pre3」、「P6_pre1」、「P6_pre2」が含まる。ＩＤ「P1_pre1」に対応する事前条件の因子条件は「入力画面．会員種別＝“ゴールド”」となる。ＩＤ「P1_pre1」に対応するその他の情報は、事前条件の関連条件文「if(n.equals(“ゴールド”)）」、事前条件関連「直接」、プログラム識別情報「CustmerRank」、ライン「９」となる。また、ＩＤ「P1_pre1」に対応するその他の情報は、事前条件の関連条件文「if（c.equals(CustmerRank.GOLD)）」、事前条件関連「間接」、プログラム識別情報「DiscountRate」、ライン「２３」となる。
【０１３９】
ＩＤ「P1_pre2」に対応する事前条件の因子条件は「入力画面．数量＞＝１０」となる。ＩＤ「P1_pre2」に対応するその他の情報は、事前条件の関連条件文「num<=10  or  num<=100」、事前条件関連「直接」、プログラム識別情報「DiscountRate」、ライン「３０」となる。ＩＤ「P1_pre3」に対応する事前条件の因子条件は「入力画面．数量＜１００」となる。ＩＤ「P1_pre3」に対応するその他の情報は、事前条件の関連条件文「num<=10  or  num<=100」、事前条件関連「直接」、プログラム識別情報「DiscountRate」、ライン「３０」となる。
【０１４０】
ＩＤ「P6_pre1」に対応する事前条件の因子条件は「入力画面．会員種別！＝“”」となる。ＩＤ「P6_pre1」に対応するその他の情報は、ＩＤ「P1_pre1」に関する情報を包含し、事前条件関連「直接」となる。ＩＤ「P6_pre2」に対応する事前条件の因子条件は「入力画面．数量＞０」となる。ＩＤ「P6_pre2」に対応するその他の情報は、事前条件の関連条件文「num<=10  or  num<=100」、事前条件関連「直接」、プログラム識別情報「DiscountRate」、ライン「３０」となる。
【０１４１】
次に、事後条件変換部２４４の処理を具体的に説明する。まず、事後条件変換部２４４は、不成立となったプロパティの事後条件をプロパティ保持部２３２から抽出し、事後条件から事後条件因子テーブルを生成する。また、事後条件変換部２４４は、プロパティが不成立となった検査対象プログラム２１０の状態において、事後条件が成立する他のプロパティを特定する。例えば、図８で説明したように、検査対象プログラム２１０が金額画面１２に遷移した場合に、プロパティ１，６の事後条件は不成立となるが、プロパティ５の事後条件は成立している。この場合、事後条件が成立する他のプロパティは、プロパティ５となる。事後条件変換部２４４は、プロパティ５の事後条件をプロパティ保持部２３２から抽出し、事後条件因子テーブルに追加する。
【０１４２】
続いて、事後条件変換部２４４が生成する事後条件因子テーブルのデータ構造の一例について説明する。図１７は、事後条件因子テーブルのデータ構造を示す図である。図１７に示すように、この事後条件因子テーブルは、プロパティ識別情報、ＩＤ、事後条件の因子条件、評価、左辺項目、右辺項目を有する。
【０１４３】
プロパティ識別情報は、プロパティを識別するものである。ＩＤは、プロパティに含まれる事後条件の因子条件を識別するものである。事後条件の因子条件は、事後条件をなす因子条件である。具体的には、プロパティ１の事後条件の因子条件は「金額画面．割引率＝１５」である。プロパティ６の事後条件の因子条件は「金額画面．金額＝金額画面．単価×金額画面．数量−金額画面．割引額」である。プロパティ５の事後条件の因子条件は「金額画面．割引額＝金額画面．単価×金額画面．数量×金額画面．割引率」となる。
【０１４４】
評価は、プロパティが不成立となったか否かを識別するものである。評価が「FALSE」の場合には、プロパティが不成立であることを示し、評価が「TRUE」の場合には、プロパティが成立していることを示す。図１７に示す例では、プロパティ１，６が「FALSE」となり、プロパティ５が「TRUE」となる。
【０１４５】
左辺項目は、事後条件の因子条件の左辺の項目を示す。具体的には、事後条件の因子条件「金額画面．割引率＝１５」の左辺項目は「金額画面．割引率」となる。事後条件の因子条件「金額画面．金額＝金額画面．単価×金額画面．数量−金額画面．割引額」の左辺項目は、「金額画面．金額」となる。事後条件の因子条件「金額画面．割引額＝金額画面．単価×金額画面．数量×金額画面．割引率」の左辺項目は「金額画面．割引額」となる。
【０１４６】
右辺項目は、事後条件の因子条件の右辺の項目を示す。事後条件の因子条件「金額画面．割引率＝１５」の右辺項目は「１５」となる。事後条件の因子条件「金額画面．金額＝金額画面．単価×金額画面．数量−金額画面．割引額」の右辺項目は「金額画面．単価」、「金額画面．数量」、「金額画面．割引額」となる。事後条件の因子条件「金額画面．割引額＝金額画面．単価×金額画面．数量×金額画面．割引率」の右辺項目は「金額画面．単価」、「金額画面．数量」、「金額画面．割引率」となる。
【０１４７】
事後条件変換部２４４は、事後条件因子テーブルに含まれる事後条件の因子条件を、検査対象プログラム２１０が利用するプログラム変数に置き換える。具体的には、事後条件変換部２４４は、パラメータ対応テーブルと事後条件因子テーブルとを比較することで、事後条件の因子条件をプログラム変数に置き換える。パラメータ対応テーブルは、図１２に示したパラメータ対応テーブルと同様である。事後条件変換部２４４は、因子条件をプログラム変数に置き換えたものを、事後因子条件変換テーブルに追加する。
【０１４８】
ここで、事後因子条件変換テーブルのデータ構造の一例について説明する。図１８は、事後因子条件変換テーブルのデータ構造を示す図である。図１８に示すように、この事後因子条件変換テーブルは、プロパティ識別情報、ＩＤ、ナンバ（Ｎｏ）、変換系列、評価、プログラム識別情報、ライン（ｌｉｎｅ）を有する。
【０１４９】
図１８において、プロパティ識別情報は、プロパティを識別するものである。ＩＤは、事後条件の因子条件を識別するものである。ナンバは、ＩＤ毎に設定される連番である。
【０１５０】
変換系列は、事後条件の因子条件の変換の過程を示すものである。後述するように、事後条件変換部２４４は、事後条件の因子条件を順次変換する。各ナンバ「１」に記憶された変換系列は、図１７に示した事後条件の因子条件そのものとなる。具体的には、ＩＤ「P1_post1」のナンバ「１」に対応する変換系列は「金額画面．割引率＝１５」となる。ＩＤ「P6_post1」のナンバ「１」に対応する変換系列は「金額画面．金額＝金額画面．単価×金額画面．数量−金額画面．割引額」となる。ＩＤ「P5_post1」のナンバ「１」に対応する変換系列は「金額画面．割引額＝金額画面．単価×金額画面．数量×金額画面．割引率」となる。
【０１５１】
各ナンバ「２」に記憶された変換系列は、各ナンバ「１」に記憶された変換系列の項目を、パラメータ対応テーブルのプログラム変数に置き換えたものとなる。具体的には、ＩＤ「P1_post1」のナンバ「２」に対応する変換系列は「rateParcent＝１５」となる。ＩＤ「P6_post1」のナンバ「２」に対応する変換系列は「total(10000)＝tanka(1000)*suryo(10)-discount(1000)」となる。ＩＤ「P5_post1」のナンバ「２」に対応する変換系列は「discount(1000)＝tanka(1000)*suryo(10)*rate(0.1)」となる。変数のカッコに含まれる数字は、図８の金額画面１２が表示された状態における変数の値である。各ナンバ「２」以降の変換系列の説明は後述する。
【０１５２】
評価は、変換系列の事後条件の因子条件が成立しているか否かを示す。各ナンバ「１」、「２」に対応する評価は、図１７に示した事後条件因子テーブルのプロパティの評価に対応させる。具体的には、プロパティ１，６のナンバ「１」、「２」の評価は「FALSE」とする。また、プロパティ５のナンバ「１」、「２」の評価は「TRUE」とする。各ナンバ「２」以降の評価の説明は後述する。
【０１５３】
プログラム識別情報は、変換系列の因子条件に関連するプログラムを識別するものである。なお、各ナンバ「１」、「２」に対応する因子条件は、プログラムから抽出したものではない。このため、各ナンバ「１」、「２」に対応するプログラム識別情報は、ブランクとする。各ナンバ「２」以降のプログラム識別情報の説明は後述する。
【０１５４】
ラインは、変換系列の因子条件に関連するプログラムの行番号を示すものである。なお、各ナンバ「１」、「２」に対応する因子条件は、プログラムから抽出したものではない。このため、各ナンバ「１」、「２」に対応するラインは、ブランクとする。各ナンバ「２」以降の行番号の説明は後述する。
【０１５５】
事後条件変換部２４４は、実行トレース情報を逆方向に辿り、事後因子条件変換テーブルの変換系列の変数を有する更新式を特定する。事後条件変換部２４４は、特定した更新式を、事後条件に関連する命令文とする。さらに、事後条件変換部２４４は、特定した更新式を、事後因子条件変換テーブルの変換系列の変数の関係を基にして変換し、変換後の変数の関係を事後因子条件変換テーブルに追加する。事後条件変換部２４４は、上記処理を繰り返し実行することで、事後条件に関連する命令文を特定する。
【０１５６】
また、事後条件変換部２４４は、実行トレース情報を逆方向に辿る場合に、最終結果となる変数の値を、事後条件の関係式に代入することで得られる値と、事後条件に関連する命令文を実行することで得られる値とを比較する。そして、事後条件変換部２４４は、各値を比較した結果、各値が等しい場合には、命令文に対する評価を「TRUE」とし、各値が異なる場合には、命令文に対する評価を「FALSE」と判定する。また、事後条件変換部２４４は、評価が「FALSE」の場合には、事後条件の変数の値と命令文とを利用して、命令文を実行する前の事後条件の値を求める。以降、事後条件変換部２４４は、命令文を実行する前の事後条件の値を求めながら、事後条件に関連する命令文を評価していく。
【０１５７】
図１９は、事後条件変換部２４４の処理を説明するための図である。図１９では、ナンバ（Ｎｏ）、プログラム識別情報、ライン（ｌｉｎｅ）、実行トレース、変数値、評価、ＩＤを用いて事後条件変換部２４４の処理を説明する。このうち、ナンバ、プログラム識別情報、ライン、実行トレース、変数値は、図１０に示したナンバ、プログラム識別情報、ライン、実行トレース、変数値と同様である。
【０１５８】
評価は、変換系列の因子条件を対応する命令文を用いて変換した場合に、変換後の変数の値が適切なものであるか否かを示すものである。変換後の変数の値が適切なものであれば「TRUE」となり、変換後の変数の値が適切なものでなければ「FALSE」となる。この評価は、図１８の評価に対応する。ＩＤは、事後条件の因子条件を識別するものである。このＩＤは、図１８のＩＤに対応する。
【０１５９】
図１９のナンバ「２９」の命令文は更新式であり、この更新式の左辺には、事後因子条件変換テーブルの変換系列の変数「discount」が含まれている。このため、事後条件変換部２４４は、ナンバ「２９」の命令文は、事後条件に関連する命令文であると判定する。
【０１６０】
続いて、事後条件変換部２４４は、ナンバ「２９」の命令文「discount=(int)(total*rate.doubleValue());」と、変換系列の「discount」に対応する変数の関係「discount(1000)=tanka(1000)*suryo(10)*rate(0.1)」とから、ナンバ「２９」の命令文を整理する。変数の関係「discount(1000)=tanka(1000)*suryo(10)*rate(0.1)」は、プロパティ５の事後条件の関係式に対応する。事後条件の関係式の各変数に格納される値は、実行トレース情報を順方向に実行した場合に、最終的に変数に格納される値である。
【０１６１】
ナンバ「２９」の命令文は「discount」を算出するものであり、変換系列の「discount」に対応する変数の関係と等しくなる。このため、
total(10000)*rate(0.1)=tanka(1000)*suryo(10)*rate(0.1)・・・式１
となる。式１の左辺の変数は、ナンバ「２９」の命令文の右辺の変数に対応する。また、式１の左辺の変数のカッコ内の数字は、順方向にプログラムを実行した場合に変数に入力される値である。式１の右辺の変数は、変換系列の「discount」に対応する変数の関係に対応する。
【０１６２】
事後条件変換部２４４が式１の各変数を整理すると、式１は、
total(10000)=tanka(1000)*suryo(10)・・・式２
となる。式２において、左辺の変数の値と右辺の変数の値はともに「１００００」となるため、式２の変数の値は適切なものである。この場合には、事後条件変換部２４４は、事後因子条件変換テーブルのＩＤ「P5_post1」のナンバ「３」に式２を追加し、評価を「TRUE」にする。また、ナンバ「２９」の命令文に対応するプログラム識別情報は、図１９に示すように「Servlet」であり、ラインは「６５」である。このため、事後条件変換部２４４は、事後因子条件変換テーブルのＩＤ「P5_post1」のナンバ「３」に対応するプログラム識別情報を「Servlet」、ラインを「６５」に設定する。
【０１６３】
図１９のナンバ「２８」の命令文は更新式であり、この更新式の右辺には、事後因子条件変換テーブルの変換系列の変数「total」が含まれている。このため、事後条件変換部２４４は、ナンバ「２８」の命令文は、事後条件に関連する命令文であると判定する。
【０１６４】
続いて、事後条件変換部２４４は、ナンバ「２８」の命令文「int  total=tanka*suryo-discount;」と、変換係数の「total」に対応する変数の関係「total(10000)=tanka(1000)*suryo(10)-discoount(1000)」とから、ナンバ「２８」の命令文を整理する。この変数の関係「total(10000)=tanka(1000)*suryo(10)-discoount(1000)」の右辺が、プロパティ６が成立する場合の事後条件に対応する。事後条件の関係式の各変数に格納される値は、実行トレース情報を順方向に実行した場合に、最終的に変数に格納される値である。
【０１６５】
ナンバ「２８」の命令文は「total」を算出するものであり、変換系列の「total」に対応する変数の関係と等しくなる。このため、
tanka(1000)*suryo(10)-discount(0)=tanka(1000)*suryo(10)-discount(1000)・・・式３
となる。式３の左辺の変数は、ナンバ「２８」の命令文の右辺の変数に対応する。また、式３の左辺の変数のカッコ内の数字は、順方向にプログラムを実行した場合に変数に入力される値である。式３の右辺の変数は、変換系列の「total」に対応する変数の関係に対応する。また、式３の右辺の変数は、プロパティ６が成立する場合の事後条件に対応する。事後条件変換部２４４は、事後因子条件変換テーブルにおいて、複数の変数の関係に該当する場合には、未選択の変数の関係のうち、ナンバが小さいものを優先して選択する。
【０１６６】
事後条件変換部２４４が式３の各変数を移項して整理すると、式３は、
discount(0)=discount(1000)・・・式４
となる。式４の左辺の変数の値は「０」であり、右辺の変数の値は「１０００」である。このため、式４は変数の値が適切ではない。この場合には、事後条件変換部２４４は、式４を、事後因子条件変換テーブルのＩＤ「P6_post1」のナンバ「３」に式４を追加し、評価を「FALSE」にする。また、ナンバ「２８」の命令文に対応するプログラム識別情報は、図１９に示すように「Servlet」であり、ラインは「６４」である。このため、事後条件変換部２４４は、事後因子条件変換テーブルのＩＤ「P6_post1」のナンバ「３」に対応するプログラム識別情報を「Servlet」、ラインを「６４」に設定する。式４の右辺が、ナンバ「２８」の命令文が実行される前の、プロパティ６の事後条件の値となる。
【０１６７】
ナンバ「２７」の命令文は更新式であり、この更新式には、事後因子条件変換テーブルの変数系列の変数「rateParcent」が含まれている。このため、事後条件変換部２４４は、ナンバ「２７」の命令文は、事後条件に関連する命令文であると判定する。
【０１６８】
続いて、事後条件変換部２４４は、ナンバ「２７」の命令文「int  rateParcent=(int)(rate.doubleValue()*100);」と、変換系列の「rateParcent」に対応する変数の関係「rateParcent=15」とから、ナンバ「２７」の命令文を整理する。この変数の関係「rateParcent=15」が、プロパティ１が成立する場合の事後条件に対応する。
【０１６９】
ナンバ「２７」の命令文は「rateParcent」を算出するものであり、変換系列の「rateParcent」に対応する変数の関係と等しくなる。このため、
(int)rate(0.1)*100=15・・・式５
となる。式５の左辺の変数は、ナンバ「２７」の命令文の右辺の変数に対応する。また、式５の左辺の変数のカッコ内の数字は、順方向にプログラムを実行した場合に変数に入力される値である。式５の右辺の値は、変換系列の「rateParcent」の右辺の値に対応する。式５の右辺の値「１５」は、プロパティ１が成立する場合の事後条件の値に対応する。
【０１７０】
事後条件変換部２４４が式５の各変数を移行して整理すると、式５は、
rate(0.1)=15/100・・・式６
となる。式６の左辺の変数の値は「０．１」であり、右辺の変数の値は「０．１５」である。このため、式６は変数の値が適切ではない。この場合には、事後条件変換部２４４は、事後因子条件変換テーブルのＩＤ「P1_post1」のナンバ「３」に式６を追加し、評価を「FALSE」にする。また、ナンバ「２７」の命令文に対応するプログラム識別情報は、図１９に示すように「Servlet」であり、ラインは「６３」である。このため、事後条件変換部２４４は、事後因子条件変換テーブルのＩＤ「P1_post1」のナンバ「３」に対応するプログラム識別情報を「Servlet」、ラインを「６３」に設定する。式６の右辺が、ナンバ「２７」の命令文が実行される前の、プロパティ１の事後条件の値となる。
【０１７１】
ナンバ「２６」の命令文は、先頭が「＜」である。このため、事後条件変換部２４４はナンバ「２６」に対する処理をスキップする。また、ナンバ「２５」の命令文は更新式でないため、事後条件変換部２４４は処理をスキップする。
【０１７２】
ナンバ「２４」の命令文は更新式であり、この更新式には、事後因子条件変換テーブルの変換係数の変数「rate」が含まれている。このため、事後条件変換部２４４は、ナンバ「２４」の命令文は、事後条件に関連する命令文であると判定する。また、ナンバ「２４」の命令文は、ナンバ「２７」に関連する命令文である。これは、ナンバ「２４」の命令文に含まれる変数「rate」が、事後因子条件変換テーブルの「rate（0.1）=0.15」に対応しており、「rate（0.1）=0.15」の右辺は、ナンバ「２７」の命令文を実行する前の事後条件の値に対応するためである。
【０１７３】
続いて、事後条件変換部２４４は、ナンバ「２４」の命令文「rate=rate.subtract(newBigDecimal(“0.05”));」と、変換系列の「rate」に対応する値「0.15」とから、ナンバ「２４」の命令文を整理する。
【０１７４】
ナンバ「２４」の命令文は「rate」を算出するものであり、変換系列の「rate」に対応する値と等しくなる。このため、
rate(0.15).subtract(newBigDecimal(“0.05”))=0.15・・・式７
となる。式７の左辺の変数は、ナンバ「２４」の命令文の右辺の変数に対応する。また、式７の左辺の変数のカッコ内の値は、順方向にプログラムを実行した場合に変数に入力される値である。式７の右辺の値は、変換系列の「rate」に対応する値である。なお、式７のsubtract(newBigDecimal(“0.05”)は、変数rateの値から「０．０５」を減算するものである。式７の右辺の値「０．１５」が、プロパティ１が成立する場合の事後条件の値に対応する。
【０１７５】
事後条件変換部２４４が式７の各変数、値を移行して整理すると、式７は、
rate(0.15)=0.20・・・式８
となる。式８の左辺の変数の値は「０．１５」であり、右辺の値は「０．２０」である。このため、式８は変数の値が適切ではない。この場合には、事後条件変換部２４４は、事後因子条件変換テーブルのＩＤ「P1_post1」のナンバ「４」に式８を追加し、評価を「FALSE」にする。また、ナンバ「２４」の命令文に対応するプログラム識別情報は、図１９に示すように「DiscountRate」であり、ラインは「３１」である。このため、事後条件変換部２４４は、事後因子条件変換テーブルのＩＤ「P1_post1」のナンバ「４」に対応するプログラム識別情報を「DiscountRate」、ラインを「３１」に設定する。式８の右辺が、ナンバ「２４」の命令文が実行される前の、プロパティ１の事後条件の値となる。
【０１７６】
ナンバ「２１〜２３」の命令文は更新式ではない。このため、事後条件変換部２４４は、ナンバ「２１〜２３」の命令文に対する処理をスキップする。
【０１７７】
ナンバ「２０」の命令文は更新式であり、この更新式には、事後因子条件変換テーブルの変数系列の変数「rate」が含まれている。このため、事後条件変換部２４４は、ナンバ「２０」の命令文は、事後条件に関連する命令文であると判定する。また、ナンバ「２０」の命令文は、ナンバ「２４」に関連する命令文である。これは、ナンバ「２０」の命令文に含まれる変数「rate」が、事後因子条件変換テーブルの「rate（0.15）=0.20」に対応しており、「rate（0.15）=0.20」の右辺は、ナンバ「２４」の命令文を実行する前の事後条件の値に対応するためである。
【０１７８】
続いて、事後条件変換部２４４は、ナンバ「２０」の命令文「rate=new  BigDecimal(“0.15”)」と、変換系列の「rate」に対応する値「０．２０」とから、ナンバ「２０」の命令文を整理する。
【０１７９】
ナンバ「２０」の命令文は「rata」を算出するものであり、変換系列の「rate」に対応する値と等しくなる。このため、
new  BigDecimal(“0.15”)=0.20・・・式９
となる。式９の左辺の変数は、ナンバ「２０」の右辺の変数に対応する。また、式９の左辺の変数のカッコ内の数字は、順方向にプログラムを実行した場合に変数に入力される値である。式９の右辺の値は、変換系列の「rate」の右辺の値に対応する。式９の右辺の値「０．２０」が、プロパティ１が成立する場合の事後条件の値に対応する。
【０１８０】
事後条件変換部２４４が式９を整理すると、式９は、
0.15=0.20・・・式１０
となる。式１０は左辺の値が「０．１５」であり、右辺の値が「０．２０」である。このため、式１０は適切ではない。この場合には、事後条件変換部２４４は、事後因子条件変換テーブルのＩＤ「P1_post1」のナンバ「５」に式１０を追加し、評価を「FALSE」にする。また、ナンバ「２０」の命令文に対応するプログラム識別情報は、図１９に示すように「DiscountRate」であり、ラインは「２５」である。このため、事後条件変換部２４４は、事後因子条件変換テーブルのＩＤ「P1_post1」のナンバ「５」に対応するプログラム識別情報を「DiscountRate」、ラインを「２５」に設定する。式１０の右辺が、ナンバ「２０」の命令文が実行される前の、プロパティ１の事後条件の値となる。
【０１８１】
ナンバ「１４〜１９」の命令文は、更新式ではないか、または、事後因子条件変換テーブルの変数系列の変数を含まない。このため、事後条件変換部２４４は、ナンバ「１４〜１９」に対する処理をスキップする。
【０１８２】
ナンバ「１３」の命令文は更新式であり、この更新式には、事後因子条件変換テーブルの変換系列の変数「suryo」が含まれている。このため、事後条件変換部２４４は、ナンバ「１３」の命令文は、事後条件に関連する命令文であると判定する。
【０１８３】
続いて、事後条件変換部２４４は、ナンバ「１３」の命令文「int  suryo=getInt(amount)」と、変換係数の「suryo」を含む変数の関係「total(10000)=tanka(1000)*suryo(10)」とから、ナンバ「１３」の命令文を整理すると、式１１のようになる。
total(10000)=tanka(1000)*getInt(amount(“10”))・・・式１１
【０１８４】
式１１では、変数の関係に含まれる変数「suryo」に、命令文の右辺の変数「getInt(amount)」を代入している。なお、変数「amount」の値は、順方向にプログラムを実行した場合に変数「amount」に入力される値である。式１１の左辺の変数の値と右辺の変数の値はともに「１００００」となる。この場合には、事後条件変換部２４４は、事後因子条件変換テーブルのＩＤ「P5_post1」のナンバ「４」に式１１を追加し、評価を「TRUE」にする。また、ナンバ「１３」の命令文に対応するプログラム識別情報は、図１９に示すように「Servlet」であり、ラインは「６１」である。このため、事後条件変換部２４４は、事後因子条件変換テーブルのＩＤ「P5_post1」のナンバ「４」に対応するプログラム識別情報を「Servlet」、ラインを「６１」に設定する。
【０１８５】
ナンバ「１２」の命令文は更新式であり、この更新式には、事後因子条件変換テーブルの変換系列の変数「tanka」が含まれている。このため、事後条件変換部２４４は、ナンバ「１３」の命令文は、事後条件に関連する命令文であると判定する。
【０１８６】
続いて、事後条件変換部２４４は、ナンバ「１２」の命令文「int  tanka=getInt(unitprice)」と、変換係数の「tanka」を含む変数の関係「total(10000)=tanka(1000)*getInt(amount(10))」とから、ナンバ「１２」の命令文を整理すると、式１２のようになる。
total(10000)=getInt(unitprice(“1000”))*getInt(amount(“10”))・・・式１２
【０１８７】
式１２では、変数の関係に含まれる変数「tanka」に、命令文の右辺の変数「getInt(unitprice)」を代入している。なお、変数「unitprice」の値は、順方向にプログラムを実行した場合に変数「unitprice」に入力される値である。式１２の左辺の変数の値と右辺の変数の値はともに「１００００」となる。この場合には、事後条件変換部２４４は、事後因子条件変換テーブルのＩＤ「P5_post1」のナンバ「５」に式１２を追加し、評価を「TRUE」にする。また、ナンバ「１２」の命令文に対応するプログラム識別情報は、図１９に示すように「Servlet」であり、ラインは「６０」である。このため、事後条件変換部２４４は、事後因子条件変換テーブルのＩＤ「P5_post1」のナンバ「５」に対応するプログラム識別情報を「Servlet」、ラインを「６０」に設定する。
【０１８８】
ナンバ「１〜１１」の命令文は、更新式ではないか、または、事後因子条件変換テーブルの変数系列の変数を含まない。このため、事後条件変換部２４４は、ナンバ「１〜１１」に対する処理をスキップする。
【０１８９】
上記のように、事後条件変換部２４４は、ナンバ「１〜２９」の命令文を逆順に辿り、図１８の事後因子条件変換テーブルを生成する。事後条件変換部２４４は、事後因子条件変換テーブルを関連命令文出力部２４５に通知する。
【０１９０】
次に、関連命令文出力部２４５が表示装置３００ｂに出力させる表示画面の一例について説明する。図２０は、関連命令文出力部２４５が表示装置に出力させる表示画面を示す図である。図２０に示すように、この表示画面は、ナンバ（Ｎｏ）、プログラム識別情報、ライン（ｌｉｎｅ）、実行トレース、変数値、事前条件関連、評価を有する。図２０に示すナンバ、プログラム識別情報、ライン、実行トレース、変数値、事前条件関連は、図１４に示したナンバ、プログラム識別情報、ライン、実行トレース、変数値、事前条件関連と同様である。また、図２０に示す評価は、図１９に示した評価と同様である。
【０１９１】
関連命令文出力部２４５は、事前条件追跡部２４３から図１５に示した事前結果テーブルを取得したとすると、不成立となったプロパティの事前条件に関連する命令文は、プログラム識別情報「CustmerRank」のライン「９」に対応する命令文である。同様に、不成立となったプロパティの事前条件に関連する命令文は、プログラム識別情報「DiscountRate」のライン「２３」に対応する命令文と、プログラム識別情報「DiscountRate」のライン「３０」に対応する命令文となる。このため、関連命令文出力部２４５は、図２０のナンバ「８」、「１８」、「２３」に対応する命令文を色つきで表示する。
【０１９２】
関連命令文出力部２４５は、事後条件変換部２４４から図１８に示した事後因子条件変換テーブルを取得したとすると、事後条件に関連する命令文は、プログラム識別情報「Servet」、ライン「６５」に対応する命令文である。また、事後条件に関連する命令文は、プログラム識別情報「Servet」、ライン「６４」に対応する命令文、プログラム識別情報「Servet」、ライン「６３」に対応する命令文、プログラム種別「DiscountRate」、ライン「３１」に対応する命令文となる。また、事後条件に関連する命令文は、プログラム識別情報「DiscountRate」、ライン「２５」に対応する命令文、プログラム識別情報「Servet」、ライン「６１」に対応する命令文、プログラム識別情報「Servet」、ライン「６０」に対応する命令文となる。このため、関連命令文出力部２４５は、図２０のナンバ「１２」、「１３」、「２０」、「２４」、「２７」、「２８」、「２９」に対応する命令文を色つきで表示する。
【０１９３】
なお、開発者等が入力装置３００ａを介して、色つきの命令文を選択した場合には、関連命令文出力部２４５は、選択された命令文に関連するソースコード、事前結果テーブル、事後因子条件変換テーブルを出力してもよい。また、関連命令文出力部２４５は、評価の「TRUE」、「FALSE」の根拠となった式１〜１２を対応する命令文とともに表示させてもよい。
【０１９４】
例えば、図２０のナンバ「８」の命令文が選択された場合には、関連命令文出力部２４５は、図４Ｂのソースコード２１０ｂを表示させるとともに、図１５に示した事前結果テーブルのナンバ「１」に対応する情報を表示する。また、図２０のナンバ「２８」の命令文が選択された場合には、関連命令文出力部２４５は、図１８に示した事後因子条件変換テーブルの「プロパティ６」に対応する情報を表示する。
【０１９５】
開発者は、表示装置３００ｂに表示された画面を参照して、検査対象プログラム２１０の誤りを判断する。開発者は、図２０の画面に色つきで表わされた命令文や、評価が「TRUE」から「FALSE」、または「FALSE」から「TRUE」に切り替わる命令文に着目すると、プログラムの誤りを見つけやすい。この場合には、図４Ａに示したソースプログラムの６Ａの各行の順番が逆になっている。すなわち、「discount=(int)(total*rate.doubleValue());)と、「int  total=tanka*suryo-discount;」とを入れ替える必要がある。また、図４Ｃに示したソースプログラムの６Ｂの「else  if(num>10)」が間違っている。正しくは「else  if(num>=10)」である。
【０１９６】
次に、本実施例２にかかるプロパティ分析装置２００の処理手順について説明する。図２１は、本実施例２にかかるプロパティ分析装置２００の処理手順を示すフローチャートである。例えば、プロパティ分析装置２００は、検査対象プログラム２１０と、この検査対象プログラム２１０に対応するプロパティ２２０が入力装置３００ａを介して記憶部２００ａに記憶された場合に、図２１に示す処理を実行する。図２１に示すように、プロパティ分析装置２００は、検査対象プログラム２１０に対してモデル検査を実行し（ステップＳ１０１）、イベント列とパラメータ列とを対応付けて記憶する（ステップＳ１０２）。
【０１９７】
プロパティ分析装置２００は、不成立となったプロパティがない場合には（ステップＳ１０３，Ｎｏ）、処理を終了する。一方、プロパティ分析装置２００は、不成立となったプロパティが有る場合には（ステップＳ１０３，Ｙｅｓ）、記憶したイベント列とパラメータ列とを用いて検査対象プログラム２１０を駆動する（ステップＳ１０４）。
【０１９８】
プロパティ分析装置２００は、不成立となったプロパティの事前条件が成立してから、事後条件が不成立となるまでの実行トレース情報を抽出する（ステップＳ１０５）。プロパティ分析装置２００は、不成立となったプロパティの事前条件に対応する変数を抽出し、抽出した変数に基づいて実行トレース情報を辿ることで、事前条件に関連する命令文を収集する（ステップＳ１０６）。
【０１９９】
プロパティ分析装置２００は、プロパティの事後条件を抽出し、実行トレース情報を逆に辿りながら事後条件に関連する命令文を収集する（ステップＳ１０７）。そして、プロパティ分析装置２００は、事前条件に関連する命令文および事後条件に関連する命令文を出力する（ステップＳ１０８）。
【０２００】
次に、図６に示したプロパティ不成立再現部２４１の処理手順について説明する。図２２は、プロパティ不成立再現部２４１の処理手順を示すフローチャートである。図２２に示す処理は、例えば、プロパティ不成立再現部２４１が、不成立となったプロパティに関連する情報をプロパティ評価部２３５から取得したことを契機にして実行される。
【０２０１】
図２２に示すように、プロパティ不成立再現部２４１は、予め設定された状態に依存するイベントとパラメータとを選択し（ステップＳ２０１）、現在の状態で未選択のイベント、パラメータが存在するか否かを判定する（ステップＳ２０２）。
【０２０２】
プロパティ不成立再現部２４１は、現在の状態で未選択のイベント、パラメータが存在する場合には（ステップＳ２０２，Ｙｅｓ）、入力されたイベント、パラメータを、状態と対応付けてスタックに格納する（ステップＳ２０３）。そして、プロパティ不成立再現部２４１は、プロパティが不成立か否かを判定する（ステップＳ２０４）。
【０２０３】
プロパティ不成立再現部２４１は、プロパティが成立する場合には（ステップＳ２０４，Ｎｏ）、ステップＳ２０１に移行する。一方、プロパティ不成立再現部２４１は、プロパティが不成立となる場合には（ステップＳ２０４，Ｙｅｓ）、不成立となったプロパティに関するイベント列およびパラメータ列をプロパティ不成立テーブルに格納し（ステップＳ２０５）、ステップＳ２０１に移行する。
【０２０４】
プロパティ不成立再現部２４１は、ステップＳ２０２において、未選択のイベント、パラメータが存在しない場合には（ステップＳ２０２，Ｎｏ）、未選択のイベントおよびパラメータが有る状態までバックトラックする（ステップＳ２０６）。
【０２０５】
プロパティ不成立再現部２４１は、バックトラック出来た場合には（ステップＳ２０７，Ｙｅｓ）、バックトラックした状態分のイベントおよびパラメータをスタックから削除し（ステップＳ２０８）、ステップＳ２０１に移行する。一方、プロパティ不成立再現部２４１は、バックトラック出来なかった場合には（ステップＳ２０７，Ｎｏ）、プロパティ不成立テーブルを出力する（ステップＳ２０９）。
【０２０６】
次に、図６に示した実行トレース収集部２４２の処理手順について説明する。図２３は、実行トレース収集部２４２の処理手順を示すフローチャートである。例えば図２３に示す処理は、実行トレース収集部２４２が、プロパティ不成立テーブルをプロパティ不成立再現部２４１から取得したことを契機にして実行される。
【０２０７】
図２３に示すように、実行トレース収集部２４２は、プロパティ不成立テーブルを取得し（ステップＳ３０１）、実行トレース情報の収集対象のプログラム範囲を設定する（ステップＳ３０２）。実行トレース収集部２４２は、プロパティ不成立テーブルから不成立となったプロパティを抽出し（ステップＳ３０３）、不成立となったプロパティに関連するイベント列およびパラメータ列をプロパティ不成立テーブルから抽出する（ステップＳ３０４）。
【０２０８】
実行トレース収集部２４２は、イベントとパラメータとがない場合には（ステップＳ３０５，Ｎｏ）、収集した実行トレース情報を出力する（ステップＳ３０６）。一方、実行トレース収集部２４２は、イベントとパラメータとが有る場合には（ステップＳ３０５，Ｙｅｓ）、イベント列およびパラメータ列からイベントおよびパラメータを順に選択して、検査対象プログラム２１０に入力する（ステップＳ３０７）。
【０２０９】
実行トレース収集部２４２は、不成立となったプロパティの事前条件が成立しない場合には（ステップＳ３０８，Ｎｏ）、ステップＳ３１０に移行する。実行トレース収集部２４２は、不成立となったプロパティの事前条件が成立する場合には（ステップＳ３０８，Ｙｅｓ）、収集対象のプログラム範囲に対して、実行トレースの収集を開始する（ステップＳ３０９）。
【０２１０】
実行トレース収集部２４２は、実行トレースの収集中であり、かつ、命令文は収集対象のプログラムの範囲内の場合には（ステップＳ３１０，Ｙｅｓ）、命令文と変数値とを実行トレース情報に格納し（ステップＳ３１１）、ステップＳ３０３に移行する。一方、実行トレース収集部２４２は、実行トレースの収集中ではない、または、命令文が収集対象のプログラム範囲外の場合には（ステップＳ３１０，Ｎｏ）、再度ステップＳ３１０に移行する。
【０２１１】
次に、図６に示した事前条件追跡部２４３の処理手順について説明する。図２４は、事前条件追跡部２４３の処理手順を示すフローチャートである。例えば図２４に示す処理は、事前条件追跡部２４３が、実行トレース情報を実行トレース収集部２４２から取得したことを契機にして実行される。
【０２１２】
図２４に示すように、事前条件追跡部２４３は、実行トレース情報を取得し（ステップＳ４０１）、不成立となったプロパティの事前条件を抽出する（ステップＳ４０２）。事前条件追跡部２４３は、事前条件因子テーブルを生成し（ステップＳ４０３）、プロパティ記述レベルがプログラム変数の場合には（ステップＳ４０４，Ｙｅｓ）、ステップＳ４０６に移行する。
【０２１３】
一方、事前条件追跡部２４３は、プロパティ記述レベルがプログラム変数ではない場合には（ステップＳ４０４，Ｎｏ）、パラメータ対応テーブルを用いてプログラム変数に変換する（ステップＳ４０５）。事前条件追跡部２４３は、プログラム変数を取得し、追跡変数リストに追加する（ステップＳ４０６）。
【０２１４】
事前条件追跡部２４３は、実行トレース情報の命令文を順方向に読み込む（ステップＳ４０７）。事前条件追跡部２４３は、命令文がある場合には（ステップＳ４０８，Ｙｅｓ）、追跡変数リストに含まれる変数を命令文が含むか否かを判定する（ステップＳ４０９）。事前条件追跡部２４３は、追跡変数リストに含まれる変数を命令文が含まない場合には（ステップＳ４０９，Ｎｏ）、ステップＳ４０７に移行する。
【０２１５】
一方、事前条件追跡部２４３は、追跡変数リストに含まれる変数を命令文が含む場合には（ステップＳ４０９，Ｙｅｓ）、該当する命令文が条件式であるか否かを判定する（ステップＳ４１０）。事前条件追跡部２４３は、該当する命令文が条件式の場合には（ステップＳ４１０，Ｙｅｓ）、該当する命令文と事前条件関連とを事前条件関連文リストに追加し（ステップＳ４１１）、ステップＳ４１４に移行する。
【０２１６】
一方、事前条件追跡部２４３は、該当する命令文が条件式以外の場合には（ステップＳ４１０，Ｎｏ）、該当する命令文が更新式であり、かつ、追跡変数リストの変数が更新式の右辺にあるか否かを判定する（ステップＳ４１２）。事前条件追跡部２４３は、該当する命令文が更新式でない場合、または、追跡変数リストの変数が更新式の右辺にない場合には（ステップＳ４１２，Ｎｏ）、ステップＳ４０７に移行する。
【０２１７】
事前条件追跡部２４３は、該当する命令文が更新式であり、かつ、追跡変数リストの変数が更新式の右辺にある場合には（ステップＳ４１２，Ｙｅｓ）、更新方法の値付きで、命令文の左辺の変数を追跡変数リストに追加する（ステップＳ４１３）。そして、事前条件追跡部２４３は、追跡変数リストの変数で、スコープから外れた変数を削除し（ステップＳ４１４）、ステップＳ４０７に移行する。
【０２１８】
ステップＳ４０８において、事前条件追跡部２４３は、命令文がない場合には（ステップＳ４０８，Ｎｏ）、事前条件関連文リストおよび事前条件因子テーブルから事前結果テーブルを生成する（ステップＳ４１５）。そして、事前条件追跡部２４３は、事前結果テーブルを出力する（ステップＳ４１６）。
【０２１９】
次に、図６に示した事後条件変換部２４４の処理手順について説明する。図２５は、事後条件変換部２４４の処理手順を示すフローチャートである。例えば図２５に示す処理は、事後条件変換部２４４が、実行トレース情報を実行トレース収集部２４２から取得したことを契機にして実行される。
【０２２０】
図２５に示すように、事後条件変換部２４４は、実行トレース情報を取得し（ステップＳ５０１）、不成立となったプロパティの事後条件の因子条件を事後条件因子テーブルに追加する（ステップＳ５０２）。
【０２２１】
事後条件変換部２４４は、不成立となったプロパティに関連する他のプロパティの事後条件の因子条件を事後条件因子テーブルに追加する（ステップＳ５０３）。事後条件変換部２４４は、プロパティ記述レベルがプログラム変数の場合には（ステップＳ５０４，Ｙｅｓ）、ステップＳ５０６に移行する。
【０２２２】
一方、事後条件変換部２４４は、プロパティ記述レベルがプログラム変数ではない場合には（ステップＳ５０４，Ｎｏ）、パラメータ対応テーブルを用いてプログラム変数に変換する（ステップＳ５０５）。そして、事後条件変換部２４４は、事後条件の因子条件を事後因子条件変換テーブルに追加する（ステップＳ５０６）。
【０２２３】
事後条件変換部２４４は、実行トレース情報の命令文をリストの末尾から逆方向に読み込み（ステップＳ５０７）、命令文があるか否かを判定する（ステップＳ５０８）。事後条件変換部２４４は、命令文がない場合には（ステップＳ５０８，Ｎｏ）、事後因子条件変換テーブルを出力する（ステップＳ５０９）。
【０２２４】
一方、事後条件変換部２４４は、命令文がある場合には（ステップＳ５０８，Ｙｅｓ）、該当する命令文が更新式であり、かつ、事後条件の因子条件の変数が左辺にあるか否かを判定する（ステップＳ５１０）。事後条件変換部２４４は、該当する命令文が更新式ではない、または、事後条件の因子条件が左辺にない場合には（ステップＳ５１０，Ｎｏ）、ステップＳ５０７に移行する。
【０２２５】
一方、事後条件変換部２４４は、該当する命令文が更新式であり、かつ、事後条件の因子条件の変数が左辺にある場合には（ステップＳ５１０，Ｙｅｓ）、該当する事後条件の因子条件を事後因子条件変換テーブルから選択する（ステップＳ５１１）。
【０２２６】
事後条件変換部２４４は、因子条件に対応する変数を更新式の右辺と置き換え（ステップＳ５１２）、置き換え済みの更新式を整理する（ステップＳ５１３）。事後条件変換部２４４は、整理した更新式を事後因子条件変換テーブルに追加する（ステップＳ５１４）。そして、事後条件変換部２４４は、更新式の評価結果を事後因子条件変換テーブルに追加し（ステップＳ５１５）、ステップＳ５０７に移行する。
【０２２７】
次に、本実施例２にかかるプロパティ分析装置２００の効果について説明する。プロパティが不成立となる場合には、プロパティの事前条件の変数を利用する条件式に誤りが存在する可能性がある。このため、事前条件追跡部２４３は、実行トレース情報を順方向に辿り、事前条件の変数を有する更新式を基にして推移後の変数を追跡する。そして、事前条件追跡部２４３は、追跡中の変数を含む条件式を抽出することで、実行トレース情報から不成立となったプロパティに関連する命令文を抽出することができる。したがって、不成立となったプロパティに関連する命令文を開発者が容易に特定することができる。
【０２２８】
また、プロパティが不成立となる場合には、プロパティの事後条件の関係式に含まれる変数の値の導出に関わった命令文に誤りが存在する可能性がある。このため、事後条件変換部２４４は、実行トレース情報を逆方向に辿り、事後条件に含まれる変数の関係式を、この関係式の変数を有する命令文を基にして順次変換し、変換後の関係式の変数を含む命令文を抽出する。したがって、不成立となったプロパティに関連する命令文を開発者が容易に特定することができる。
【０２２９】
また、事後条件変換部２４４は、事後条件に含まれる変数の関係式から導かれる値と、この関係式の変数を含む命令文が実行された場合の値とを比較し、比較結果と抽出した命令文とを対応付けて出力する。比較結果が「TRUE」から「FALSE」に変化する部分の命令文または、比較結果が「FALSE」から「TRUE」に変化する部分の命令文に誤りが存在する可能性が高い。このため、開発者が比較結果と命令文とを利用することで、不成立となったプロパティに関連する命令文をより特定しやすくすることができる。
【０２３０】
ところで、図２に示したプロパティ分析装置２００の各構成要素は機能概念的なものであり、必ずしも物理的に図示の如く構成されていることを要しない。すなわち、プロパティ分析装置２００の分散、統合の具体的形態は図示のものに限られず、その全部または一部を、各種の負担や使用状況等に応じて、任意の単位で機能的または物理的に分散、統合して構成することができる。例えば、記憶部２００ａを、着脱可能な外部装置に搭載し、この外部装置にプロパティ分析装置２００が有線または無線で接続するようにしてもよい。
【０２３１】
上記のプログラム駆動部２３３は、検査対象プログラム保持部２３１に記憶された検査対象プログラム２１０を駆動させていたがこれに限定されるものではない。例えば、プログラム駆動部２３３は、記憶部２００ａから検査対象プログラム２１０を直接取得し、この検査対象プログラム２１０を駆動させてもよい。
【０２３２】
上記のプロパティ評価部２３５は、プロパティ保持部２３２に記憶されたプロパティ２２０を利用して、プロパティが成立するか否かを判定していたがこれに限定されるものではない。例えば、プロパティ評価部２３５は、記憶部２２０ａからプロパティ２２０を直接取得し、プロパティが成立するか否かを判定してもよい。
【０２３３】
上記の事前条件追跡部２４３は、実行トレース情報を順方向に辿りながら変数の推移関係を追跡し、追跡中の変数を含む条件式を事前条件関連文リストに追加する場合について説明したが、これに限定されるものではない。例えば、事前条件追跡部２４３は、追跡中の変数を含む更新式を不成立となったプロパティに関連する命令文として特定してもよい。
【０２３４】
上記の事前条件追跡部２４３は、追跡変数リストの変数を処理する条件式であり、かつ、条件式の変数が「TRUE」となる命令文を、不成立となったプロパティに関連する命令文として特定していたが、これに限定されるものではない。例えば、事前条件追跡部２４３は、追跡変数リストの変数を処理する条件式であり、かつ、条件式の変数が「FALSE」となる命令文を、不成立となったプロパティに関連する命令文として特定してもよい。
【０２３５】
上記の事後条件変換部２４４は、実行トレース情報を逆方向に辿り、事後条件に含まれる変数の関係式を、この関係式の変数を有する命令文を基にして順次変換し、変換後の関係式の変数を含む命令文を抽出する。また、事後条件変換部２４４は、事後条件に含まれる変数の関係式から導かれる値と、この関係式の変数を含む命令文が実行された場合の値とを比較し、比較結果と抽出した命令文とを対応付けて出力していた。しかし、事後条件変換部２４４の処理の一部を代わりに実行する比較部を更に設けてもよい。例えば、この比較部は、事後条件変換部２４４が抽出した命令文が実行された場合の値と、該命令文に対応するプロパティの事後条件に含まれる変数の関係式から導かれる値とを比較し、比較結果と命令文とを対応付けて出力する。
【０２３６】
なお、上記のプロパティ分析装置２００は、既知のパーソナルコンピュータ、ワークステーション、携帯電話、ＰＨＳ、移動体通信端末またはＰＤＡ等の情報処理装置に、プロパティ分析装置２００の各機能を搭載することによって実現することもできる。
【０２３７】
図２６は、本実施例にかかるプロパティ分析装置を構成するコンピュータのハードウェア構成を示す図である。図２６に示すように、このコンピュータ４００は、各種演算処理を実行するＣＰＵ４０１と、ユーザからのデータの入力を受け付ける入力装置４０２と、モニタ４０３を有する。また、コンピュータ４００は、記憶媒体からプログラム等を読取る媒体読み取り装置４０４と、ネットワークを介して他のコンピュータとの間でデータの授受を行うネットワークインターフェース装置４０５とを有する。また、コンピュータ４００は、各種情報を一時記憶するＲＡＭ（Random  Access  Memory）４０６と、ハードディスク装置４０７とを有する。各装置４０１〜４０７は、バス４０８に接続される。
【０２３８】
そして、ハードディスク装置４０７は、図２に示したプロパティ分析装置２００と同様の機能を有するモデル検査プログラム４０７ａとプロパティ不成立分析プログラム４０７ｂとを記憶する。また、ハードディスク装置４０７は、図２に示した検査対象プログラム２１０、プロパティ２２０にそれぞれ対応する検査対象プログラム４０７ｃ、プロパティ４０７ｄを記憶する。
【０２３９】
ＣＰＵ４０１は、モデル検査プログラム４０７ａ、プロパティ不成立分析プログラム４０７ｂを読み出してＲＡＭ４０６に展開する。そうすると、モデル検査プログラム４０７ａは、モデル検査プロセス４０６ａとして機能し、プロパティ不成立分析プログラム４０７ｂは、プロパティ不成立分析プロセス４０６ｂとして機能するようになる。モデル検査プロセス４０６ａは、図２のモデル検査部２３０に対応し、プロパティ不成立分析プロセス４０６ｂは、図２のプロパティ不成立分析部２４０に対応する。なお、ＣＰＵ４０１は、ハードディスク装置４０７に記憶された検査対象プログラム４０７ｃ、プロパティ４０７ｄを読み出して、ＲＡＭ４０６に記憶させる。モデル検査プロセス４０６ａおよびプロパティ不成立分析プロセス４０６ｂは協働し、プロパティ４０６ｄに関連する命令文を検査対象プログラム４０６ｃから抽出し、モニタ４０３に表示させる。
【０２４０】
なお、モデル検査プログラム４０７ａ、プロパティ不成立分析プログラム４０７ｂ、検査対象プログラム４０７ｃ、プロパティ４０７ｄは、必ずしもハードディスク装置４０７に格納されている必要はない。コンピュータ４００は、ＣＤ−ＲＯＭ等の記憶媒体に記憶された各データ４０７ａ〜４０７ｄを読み出して実行するようにしてもよい。また、公衆回線、インターネット、ＬＡＮ（Local  Area  Network）、ＷＡＮ（Wide  Area  Network）等にこの各データ４０７ａ〜４０７ｄを記憶させておき、コンピュータ４００がこれらから各データ４０７ａ〜４０７ｄを読み出して実行するようにしてもよい。
【０２４１】
以上の各実施例を含む実施形態に関し、さらに以下の付記を開示する。
【０２４２】
（付記１）モデルの状態が遷移する前の入力データの条件を示す事前条件および前記モデルの状態が遷移した後のモデルの状態の条件を変数の関係式で示した事後条件を含むプロパティと、入力データに対して実行される前記モデルの命令文を含む実行トレースとを記憶する記憶部と、
前記実行トレースに含まれる命令文を順方向に辿り、前記プロパティの事前条件に対応する変数を含み結果が真となる条件式を抽出する第１の抽出部と、
前記プロパティの事後条件の関係式に含まれる変数の値の導出に関わった命令文を逆方向から辿り、該関係式を含む命令文を抽出する第２の抽出部と
を備えたことを特徴とするプロパティ分析装置。
【０２４３】
（付記２）前記第１の抽出部は、前記実行トレースの命令文を順方向に辿る際に、前記プロパティの事前条件の変数の推移関係を表す更新式を基にして推移後の変数を追跡し、追跡中の変数を含む命令文を抽出することを特徴とする付記１に記載のプロパティ分析装置。
【０２４４】
（付記３）前記第２の抽出部は、前記実行トレースの命令文を逆方向に辿る際に、前記プロパティの事後条件に含まれる変数の関係式を、該関係式の変数を有する命令文を基にして順次変換し、変換後の関係式の変数を含む命令文を抽出することを特徴とする付記１または２に記載のプロパティ分析装置。
【０２４５】
（付記４）前記第２の抽出部が抽出した命令文が実行された場合の値と、該命令文に対応する前記プロパティの事後条件に含まれる変数の関係式から導かれる値とを比較し、比較結果と前記第２の抽出部が抽出した命令文とを対応付ける比較部を更に有することを特徴とする付記１、２または３に記載のプロパティ分析装置。
【０２４６】
（付記５）前記比較部による比較の結果、値が一致しない場合には、前記関係式に関連するプロパティを成立させる値を基に、前記第２の抽出部が抽出した命令文の処理前の値を求め、その値を事後条件に含まれる変数の関係式から導かれる値と置き換えて順次比較を行うことを特徴とする付記４に記載のプロパティ分析装置。
【０２４７】
（付記６）プロパティ分析装置が、
入力データに対して実行されるモデルの実行トレースに含まれる命令文を順方向に辿り、モデルの状態が遷移する前の入力データの条件を示す事前条件および前記モデルの状態が遷移した後のモデルの状態の条件を変数の関係式で示した事後条件を含むプロパティの前記事前条件に対応する変数を含み結果が真となる条件式を抽出する第１の抽出ステップと、
前記プロパティの事後条件の関係式に含まれる変数の値の導出に関わった命令文を逆方向から辿り、該関係式を含む命令文を抽出する第２の抽出ステップと
を含むことを特徴とするプロパティ分析方法。
【０２４８】
（付記７）前記第１の抽出ステップは、前記実行トレースの命令文を順方向に辿る際に、前記プロパティの事前条件の推移関係を表す更新式を基にして推移後の変数を追跡し、追跡中の変数を含む命令文を抽出することを特徴とする付記６に記載のプロパティ分析方法。
【０２４９】
（付記８）前記第２の抽出ステップは、前記実行トレースの命令文を逆方向に辿る際に、前記プロパティの事後条件に含まれる変数の関係式を、該関係式の変数を有する命令文を基にして順次変換し、変換後の関係式の変数を含む命令文を抽出することを特徴とする付記６または７に記載のプロパティ分析方法。
【０２５０】
（付記９）前記第２の抽出ステップにて抽出した命令文が実行された場合の値と、該命令文に対応する前記プロパティの事後条件に含まれる変数の関係式から導かれる値とを比較し、比較結果と前記第２の抽出ステップにて抽出された命令文とを対応付ける比較ステップを更に含むことを特徴とする付記６、７または８に記載のプロパティ分析方法。
【０２５１】
（付記１０）コンピュータに、
入力データに対して実行されるモデルの実行トレースに含まれる命令文を順方向に辿り、モデルの状態が遷移する前の入力データの条件を示す事前条件および前記モデルの状態が遷移した後のモデルの状態の条件を変数の関係式で示した事後条件を含むプロパティの前記事前条件に対応する変数を含み結果が真となる条件式を抽出する第１の抽出手順と、
前記プロパティの事後条件の関係式に含まれる変数の値の導出に関わった命令文を逆方向から辿り、該関係式を含む命令文を抽出する第２の抽出手順と
を実行させることを特徴とするプロパティ分析プログラム。
【０２５２】
（付記１１）前記第１の抽出手順は、前記実行トレースの命令文を順方向に辿る際に、前記プロパティの事前条件の推移関係を表す更新式を基にして推移後の変数を追跡し、追跡中の変数を含む命令文を抽出することを特徴とする付記１０に記載のプロパティ分析プログラム。
【０２５３】
（付記１２）前記第２の抽出手順は、前記実行トレースの命令文を逆方向に辿る際に、前記プロパティの事後条件に含まれる変数の関係式を、該関係式の変数を有する命令文を基にして順次変換し、変換後の関係式の変数を含む命令文を抽出することを特徴とする付記１０または１１に記載のプロパティ分析プログラム。
【０２５４】
（付記１３）前記第２の抽出手順にて抽出した命令文が実行された場合の値と、該命令文に対応する前記プロパティの事後条件に含まれる変数の関係式から導かれる値とを比較し、比較結果と前記第２の抽出手順にて抽出された命令文とを対応付ける比較手順を更にコンピュータに実行させることを特徴とする付記１０、１１または１２に記載のプロパティ分析プログラム。
【符号の説明】
【０２５５】
１００    プロパティ分析装置
１１０    記憶部
１１０ａ  プロパティ
１１０ｂ  実行トレース
１２０    第１の抽出部
１３０    第２の抽出部
【図１】
0005471718.tif 000002
【図２】
0005471718.tif 000003
【図３】
0005471718.tif 000004
【図４Ａ】
0005471718.tif 000005
【図４Ｂ】
0005471718.tif 000006
【図４Ｃ】
0005471718.tif 000007
【図５】
0005471718.tif 000008
【図６】
0005471718.tif 000009
【図７】
0005471718.tif 000010
【図８】
0005471718.tif 000011
【図９】
0005471718.tif 000012
【図１０】
0005471718.tif 000013
【図１１】
0005471718.tif 000014
【図１２】
0005471718.tif 000015
【図１３】
0005471718.tif 000016
【図１４】
0005471718.tif 000017
【図１５】
0005471718.tif 000018
【図１６】
0005471718.tif 000019
【図１７】
0005471718.tif 000020
【図１８】
0005471718.tif 000021
【図１９】
0005471718.tif 000022
【図２０】
0005471718.tif 000023
【図２１】
0005471718.tif 000024
【図２２】
0005471718.tif 000025
【図２３】
0005471718.tif 000026
【図２４】
0005471718.tif 000027
【図２５】
0005471718.tif 000028
【図２６】
0005471718.tif 000029
【図２７】
0005471718.tif 000030
【図２８】
0005471718.tif 000031