【手続補正書】
【提出日】平成29年2月24日(2017.2.24)
【手続補正１】
【補正対象書類名】特許請求の範囲
【補正対象項目名】全文
【補正方法】変更
【補正の内容】
【特許請求の範囲】
【請求項１】
入力値にしたがって内部状態値を更新するとともに前記入力値に対応する出力値を出力する処理を実装した動的プログラムを検査するプログラム検査装置であって、
指定した制約条件を充足することができる解を求めることにより前記動的プログラムの前記入力値、前記内部状態値、および前記出力値を検査するＳＡＴソルバを備え、
前記ＳＡＴソルバは、
前記内部状態値を前記動的プログラムに保持させつつ入力値列内の入力値を前記動的プログラムに対して順次引き渡して実行することにより求められる前記動的プログラムの内部状態値列と出力値列を前記入力値列とともに記述した動的プログラム記述、
前記入力値列が満たすべき検査条件、前記内部状態値列が満たすべき検査条件、および前記出力値列が満たすべき検査条件の少なくともいずれかを記述した検査条件記述、
を前記制約条件として受け取り、前記制約条件に違反する前記入力値列、前記制約条件に違反する前記内部状態値列の初期値、および前記制約条件に違反する前記出力値列の少なくともいずれかが存在するか否かを前記解として探索し、前記解が存在しない場合はその旨の処理結果を出力し、前記解が存在する場合はその解に対応する前記入力値列、前記内部状態値列、および前記出力値列を出力する
ことを特徴とするプログラム検査装置。
【請求項２】
前記ＳＡＴソルバは、前記制約条件としてさらに、
前記内部状態値の初期値が満たすべき条件を記述した初期値制約条件記述、および
前記動的プログラムに対して引き渡す前記入力値列が満たすべき条件を記述した入力値列制約条件記述、
を受け取り、
前記ＳＡＴソルバは、
前記検査条件を満たす前記解が存在しない場合は前記検査条件自体が適正でない旨の処理結果を出力し、
前記初期値制約条件記述が記述する条件を満たす前記解が存在しない場合はその条件自体が適正でない旨の処理結果を出力し、
前記入力値列制約条件記述が記述する条件を満たす前記解が存在しない場合はその条件自体が適正でない旨の処理結果を出力する
ことを特徴とする請求項１記載のプログラム検査装置。
【請求項３】
前記検査条件、および前記入力値列制約条件記述が記述している条件は、前記入力値列内の入力値毎に定義されている
ことを特徴とする請求項２記載のプログラム検査装置。
【請求項４】
請求項１記載のプログラム検査装置を用いて前記動的プログラムを検査するソフトウェア装置であって、
前記内部状態値を前記動的プログラムに保持させつつ入力値列内の入力値を前記動的プログラムに対して順次引き渡して実行することにより前記内部状態値列と前記出力値列を求める検査用プログラム構築部、
前記入力値列が満たすべき検査条件、前記内部状態値列が満たすべき検査条件、および前記出力値列が満たすべき検査条件の少なくともいずれかを受け取り、前記検査条件記述に変換する、検査条件設定部、
を備え、
前記検査用プログラム構築部は、求めた前記内部状態値列と前記出力値列を前記動的プログラム記述として前記プログラム検査装置に対して引き渡し、
前記検査条件設定部は、前記変換した検査条件記述を前記プログラム検査装置に対して引き渡す
ことを特徴とするソフトウェア検査装置。
【請求項５】
請求項２記載のプログラム検査装置を用いて前記動的プログラムを検査するソフトウェア装置であって、
前記内部状態値を前記動的プログラムに保持させつつ入力値列内の入力値を前記動的プログラムに対して順次引き渡して実行することにより前記内部状態値列と前記出力値列を求める検査用プログラム構築部、
前記入力値列が満たすべき検査条件、前記内部状態値列が満たすべき検査条件、および前記出力値列が満たすべき検査条件の少なくともいずれかを受け取り、前記検査条件記述に変換する、検査条件設定部、
前記内部状態値の初期値が満たすべき条件を受け取り、前記初期値制約条件記述に変換する、初期値制約設定部、
前記動的プログラムに対して引き渡す前記入力値列が満たすべき条件を受け取り、前記入力値列制約条件記述に変換する、入力値列制約設定部、
を備え、
前記検査用プログラム構築部は、求めた前記内部状態値列と前記出力値列を前記動的プログラム記述として前記プログラム検査装置に対して引き渡し、
前記検査条件設定部は、前記変換した検査条件記述を前記プログラム検査装置に対して引き渡し、
前記初期値制約設定部は、前記変換した初期値制約条件記述を前記プログラム検査装置に対して引き渡し、
前記入力値列制約設定部は、前記変換した入力値列制約条件記述を前記プログラム検査装置に対して引き渡す
ことを特徴とするソフトウェア検査装置。
【請求項６】
前記検査条件設定部は、前記入力値列、前記内部状態値列、および前記出力値列のうち少なくともいずれかが満たすべき前提条件および拘束条件を、論理演算式の形式で前記検査条件記述として生成する
ことを特徴とする請求項４記載のソフトウェア検査装置。
【請求項７】
前記入力値制約設定部は、前記入力値列が満たすべき前提条件および拘束条件を、論理演算式の形式で前記入力値列制約条件記述として生成し、
前記初期値制約設定部は、前記内部状態値の初期値が満たすべき前提条件および拘束条件を、論理演算式の形式で前記初期値制約条件記述として生成する
ことを特徴とする請求項５記載のソフトウェア検査装置。
【請求項８】
前記検査条件設定部は、ビット論理演算式の形式で前記検査条件記述を生成する
ことを特徴とする請求項６記載のソフトウェア検査装置。
【請求項９】
前記入力値制約設定部は、ビット論理演算式の形式で前記入力値列制約条件記述を生成し、
前記初期値制約設定部は、ビット論理演算式の形式で前記初期値制約条件記述を生成する
ことを特徴とする請求項７記載のソフトウェア検査装置。
【請求項１０】
指定した制約条件を充足することができる解を求めることにより、入力値にしたがって内部状態値を更新するとともに前記入力値に対応する出力値を出力する処理を実装した動的プログラムの前記入力値、前記内部状態値、および前記出力値を検査するＳＡＴソルバに対して入力する前記制約条件を記述したＳＡＴ制約条件データであって、
前記内部状態値を前記動的プログラムに保持させつつ入力値列内の入力値を前記動的プログラムに対して順次引き渡して実行することにより求められる前記動的プログラムの内部状態値列と出力値列を前記入力値列とともに記述した動的プログラム記述、
前記入力値列が満たすべき検査条件、前記内部状態値列が満たすべき検査条件、および前記出力値列が満たすべき検査条件の少なくともいずれかを記述した検査条件記述、
を含み、
前記検査条件記述は、前記入力値列、前記内部状態値列、および前記出力値列のうち少なくともいずれかが満たすべき前提条件および拘束条件を、論理演算式の形式で記述している
ことを特徴とするＳＡＴ制約条件データ。
【請求項１１】
前記ＳＡＴ制約条件データはさらに、
前記内部状態値の初期値が満たすべき条件を記述した初期値制約条件記述、および
前記動的プログラムに対して引き渡す前記入力値列が満たすべき条件を記述した入力値列制約条件記述、
を含み、
前記入力値列制約条件記述は、前記入力値列が満たすべき前提条件および拘束条件を、論理演算式の形式で記述しており、
前記初期値制約条件記述は、前記内部状態値の初期値が満たすべき前提条件および拘束条件を、論理演算式の形式で記述している
ことを特徴とする請求項１０記載のＳＡＴ制約条件データ。
【請求項１２】
請求項１０記載のＳＡＴ制約条件データを格納したことを特徴とする記憶媒体。