"プログラムのテストに用いられるデータベース内のテストデータについての制約を表す第1の制約データを格納する第1データ格納部に格納されている前記第1の制約データに含まれる、前記テストデータに含まれるべきレコードの選択に関する制約であるレコード選択制約に従って選択したレコードが満たすべき制約であるレコード単位制約についての第1の表現パターンを、未解釈関数で置換することによって第2の制約データを生成し、第2データ格納部に格納する第1制約生成ステップと、前記第2データ格納部に格納されている前記第2の制約データに対する充足可能性判定処理を充足可能性判定処理部に実施させ、前記第1の制約データについての第1の充足値を前記充足可能性判定処理部から取得し、第3データ格納部に格納するステップと、前記第3データ格納部に格納されている前記第1の充足値と、前記第1の制約データに含まれる第1の表現パターンと、前記第1の制約データに含まれる、前記第1の表現パターン以外の制約についての第2の表現パターンとから、前記レコード単位制約についての第3の制約データを生成し、第4データ格納部に格納する第2制約生成ステップと、前記第4データ格納部に格納されている前記第3の制約データに対する充足可能性判定処理を充足可能性判定処理部に実施させ、前記第3の制約データについての第2の充足値を前記充足可能性判定処理部から取得し、第4データ格納部に格納するステップと、を、コンピュータに実行させるためのテストデータ生成プログラム。前記第1の制約データに含まれる文字列変数を数値型の変数に変換する変換ステップと、前記第4データ格納部に格納されている前記第2の充足値に含まれ且つ前記変換ステップで変換された、前記数値型の変数の値を、文字列に変換するステップと、を、さらに前記コンピュータに実行させるための請求項1記載のテストデータ生成プログラム。前記第2制約生成ステップが、前記第1の充足値に含まれる前記未解釈関数の入出力対応データから、前記第1の表現パターンの各々の真偽を特定し、前記第1の表現パターンの各々と対応する真偽との組み合わせについての制約を生成する第1生成ステップと、前記第1の充足値から、前記第2の表現パターンの各々の真偽を特定し、前記第2の表現パターンの各々と対応する真偽との組み合わせについての制約を生成する第1生成ステップと、前記第1の充足値に含まれる前記データベース内の各レコードの値を表す制約と、前記第1生成ステップ及び前記第2生成ステップで生成された制約とを含む制約データを生成するステップと、を含む請求項1又は2記載のテストデータ生成プログラム。前記第1生成ステップが、前記第1の表現パターンの各々と対応する真偽との組み合わせについての制約を、第1の表現パターンに関連する制約定義に従って展開するステップをさらに含む請求項3記載のテストデータ生成プログラム。プログラムのテストに用いられるデータベース内のテストデータについての制約を表す第1の制約データを格納する第1データ格納部に格納されている前記第1の制約データにおいて、前記テストデータに含まれるべきレコードの選択に関する制約であるレコード選択制約に従って選択したレコードが満たすべき制約であるレコード単位制約についての第1の表現パターンを、未解釈関数で置換することによって第2の制約データを生成し、第2データ格納部に格納する第1制約生成ステップと、前記第2データ格納部に格納されている前記第2の制約データに対して充足可能性判定処理を実施し、前記第1の制約データについての第1の充足値を取得し、第3データ格納部に格納するステップと、前記第3データ格納部に格納されている前記第1の充足値と、前記第1の制約データに含まれる第1の表現パターンと、前記第1の制約データに含まれる、前記第1の表現パターン以外の制約についての第2の表現パターンとから、前記レコード単位制約についての第3の制約データを生成し、第4データ格納部に格納する第2制約生成ステップと、前記第4データ格納部に格納されている前記第3の制約データに対して充足可能性判定処理を実施し、前記第3の制約データについての第2の充足値を取得し、第4データ格納部に格納するステップと、を含み、コンピュータにより実行されるテストデータ生成方法。プログラムのテストに用いられるデータベース内のテストデータについての制約を表す第1の制約データを格納する第1データ格納部に格納されている前記第1の制約データにおいて、前記テストデータに含まれるべきレコードの選択に関する制約であるレコード選択制約に従って選択したレコードが満たすべき制約であるレコード単位制約についての第1の表現パターンを、未解釈関数で置換することによって第2の制約データを生成し、第2データ格納部に格納する手段と、充足可能性判定処理部と、前記第2データ格納部に格納されている前記第2の制約データに対して充足可能性判定処理を前記充足可能性判定処理部に実施させ、前記第1の制約データについての第1の充足値を前記充足可能性判定処理部から取得し、第3データ格納部に格納する処理手段と、前記第3データ格納部に格納されている前記第1の充足値と、前記第1の制約データに含まれる第1の表現パターンと、前記第1の制約データに含まれる、前記第1の表現パターン以外の制約についての第2の表現パターンとから、前記レコード単位制約についての第3の制約データを生成し、第4データ格納部に格納する手段と、を有し、前記処理手段は、前記第4データ格納部に格納されている前記第3の制約データに対して充足可能性判定処理を前記充足可能性判定処理部に実施させ、前記第3の制約データについての第2の充足値を前記充足可能性判定処理部から取得し、第4データ格納部に格納する、テストデータ生成装置。従って、本技術の目的は、一側面において、テストデータを高速に生成するための技術を提供することである。本テストデータ生成方法は、Aプログラムのテストに用いられるデータベース内のテストデータについての制約を表す第1の制約データを格納する第1データ格納部に格納されている第1の制約データに含まれる、テストデータに含まれるべきレコードの選択に関する制約であるレコード選択制約に従って選択したレコードが満たすべき制約であるレコード単位制約についての第1の表現パターンを、未解釈関数で置換することによって第2の制約データを生成し、第2データ格納部に格納する第1制約生成ステップと、B第2データ格納部に格納されている第2の制約データに対する充足可能性判定処理を充足可能性判定処理部に実施させ、第1の制約データについての第1の充足値を充足可能性判定処理部から取得し、第3データ格納部に格納するステップと、C第3データ格納部に格納されている第1の充足値と、第1の制約データに含まれる第1の表現パターンと、第1の制約データに含まれる、第1の表現パターン以外の制約についての第2の表現パターンとから、レコード単位制約についての第3の制約データを生成し、第4データ格納部に格納する第2制約生成ステップと、D第4データ格納部に格納されている第3の制約データに対する充足可能性判定処理を充足可能性判定処理部に実施させ、第3の制約データについての第2の充足値を充足可能性判定処理部から取得し、第4データ格納部に格納するステップとを含む。テストデータを高速に生成することができるようになる。以下、本技術の実施の形態を詳細に説明するが、実施の形態の説明が分かりやすくなるように、以下に示すような具体例に沿って処理を説明するものとする。すなわち、在庫管理システムの一部についてテストを行うことを想定する。より具体的には、図1に示すように、商品検索画面において商品名の入力欄に、例えばABCといった商品名についての文字列を入力し、検索ボタンをクリックして、在庫管理システムに商品検索を行わせる場合のテストを想定する。ここで、商品名ABCに完全一致する商品名の在庫データだけを抽出するのであれば従来技術でも十分対応可能であるが、入力された文字列に前方一致する商品名についても抽出する場合には、以下で述べるような本実施の形態を用いる方が、高速にテストデータを生成することができる。本具体例では、前方一致を取り扱うことにする。本具体例の在庫管理システムは、商品名及び単価を保持する商品マスタテーブルと、商品名及び在庫数を保持する在庫状況テーブルとをデータベースとして管理している。このような在庫管理システムは、例えば図1のような検索の指示に応じて、A複数の商品が抽出されて在庫もある場合に図2に示すような商品検索結果画面を出力する、B1つの商品のみが抽出されて在庫もある場合に図3に示すような商品発注画面を出力する、C1つの商品も抽出されず又は1つの商品のみ抽出されたが在庫がない場合エラー画面を出力する、のいずれかの処理を実施する。それぞれについてテストデータを生成することになるが、本具体例では、Bの場合のためのテストデータを生成することにする。この場合のテスト項目は以下のとおりである。商品検索画面で検索ボタン押下時に、1入力された商品名に前方一致する商品が商品マスタテーブルにただ1件存在し、且つ2当該商品に対応する在庫状況テーブルの在庫数が1以上の場合、該当する商品の発注画面が表示される。また、商品マスタテーブル及び在庫状況テーブルについてのER多重度制約は、以下のとおりである。3商品マスタテーブルの全てのレコードに対して、商品が対応する在庫状況テーブルのレコードが0件又は1件存在し、且つ4在庫状況テーブルの全てのレコードに対して、商品が対応する商品マスタテーブルのレコードが1件存在する。従来技術によれば、このようなテスト項目及びER制約に応じた制約データを自動的に生成することができ、本具体例については例えば図4に示すような制約データが得られる。なお、ここでは商品マスタテーブルの最大レコード数が3に設定されており、在庫状況テーブルの最大レコード数が2に設定されている。但し、prefixは、YがXに前方一致するという論理関数を表している。図4の例では、1及び2に関する制約の組み合わせが3セット、3に関する制約が3セット、4に関する制約が2セット含まれている。1及び2に関する制約の組み合わせについてはOR条件で連結されており、3に関する制約はAND条件で連結されており、4に関する制約もAND条件で連結されている。さらに、1及び2に関する制約の組み合わせ全体と、3に関する制約と、4に関する制約とは、ANDで連結されている。1及び2に関する制約の組み合わせの最初のものは、入力された商品名が、商品マスタテーブルの0番目のレコードにおける商品カラムの値と一致しており、且つ商品マスタテーブルの0番目のレコードにおける商品カラムの値と在庫状況テーブルの0番目のレコードにおける商品カラムの値と一致し且つ在庫状況テーブルの0番目のレコードにおける在庫数が1以上であるか、又は商品マスタテーブルの0番目のレコードにおける商品カラムの値と在庫状況テーブルの1番目のレコードにおける商品カラムの値と一致し且つ在庫状況テーブルの1番目のレコードにおける在庫数が1以上である、という制約を表している。以下、商品マスタテーブルの1番目が該当する場合と、2番目が該当する場合とについて制約が規定されている。3に関する制約の最初のものは、商品マスタテーブルの0番目のレコードにおける商品カラムの値と在庫状況テーブルの0番目のレコードにおける商品カラムの値とが一致しているという論理が偽であるか、又は商品マスタテーブルの0番目のレコードにおける商品カラムの値と在庫状況テーブルの1番目のレコードにおける商品カラムの値とは一致しているという論理が偽である、という制約を規定している。これは、3の制約が0件又は1件という条件となっているためである。以下、商品マスタテーブルの1番目のレコード、2番目のレコードについての制約が規定されている。4に関する制約の最初のものは、在庫状況テーブルの0番目のレコードにおける商品カラムの値と商品マスタテーブルの0番目のレコードにおける商品カラムの値が一致するか、在庫状況テーブルの0番目のレコードにおける商品カラムの値と商品マスタテーブルの1番目のレコードにおける商品カラムの値が一致するか、又は在庫状況テーブルの0番目のレコードにおける商品カラムの値と商品マスタテーブルの2番目のレコードにおける商品カラムの値が一致するか、という制約を規定している。以下、在庫状況テーブルの1番目のレコードについての制約も規定されている。なお、図4では、分かりやすいようにprefixという論理関数を導入しているが、実際には、各prefixの論理関数は図5のように展開される制約となる。具体的には、prefixは、文字列Xの長さを出力する関数である。ここでは最大文字数を5に限定している。図5に示した制約は、以下のような事項を規定したものである。商品名の長さが1で、商品マスタ0商品の1文字目に一致or商品名の長さが2で、商品マスタ0商品の1及び2文字目に一致or商品名の長さが3で、商品マスタ0商品の1乃至3文字目に一致or商品名の長さが4で、商品マスタ0商品の1乃至4文字目に一致or商品名の長さが5で、商品マスタ0商品の1乃至5文字目に一致このように制約データには、どのレコードが条件を満たすのかというレコードの選択に関する制約レコード選択制約と呼ぶと、選択したレコードが満たすべき制約レコード単位制約とが含まれている。本具体例では、prefixという論理関数で表している部分がレコード単位制約を表しており、それ以外の部分がレコード選択制約となっている。このprefixは、本具体例でも9つ含まれており、これを全て展開すると、非常に複雑な制約になることが分かる。このように、レコード選択制約とレコード単位制約とを同時に解こうとすると、制約が複雑化してしまい、SMTソルバの処理時間が長くなってしまう。本実施の形態では、以下で詳細に述べるように、レコード選択制約を先に解いて、その結果を用いてレコード単位制約を再構成して解くという手法を採用する。このように、1回に解くべき制約を単純化して、個々の制約についての処理時間を短縮することで、全体としての処理時間をも短縮する。以下、このような手法を実際に行う際の構成及び処理について説明する。図6に、本技術の実施の形態に係るシステムの概要を示す。本実施の形態に係るテストデータ生成装置100は、元制約データ格納部103と、型情報格納部104と、制約語彙定義格納部105と、未解釈関数割当部106と、第1データ格納部107と、制約変換部108と、第2データ格納部109と、SMTソルバインタフェース部110と、第3データ格納部111と、充足値反映部112と、第4データ格納部113と、制約構成部114と、第5データ格納部115と、第6データ格納部116と、充足値変換部117と、第7データ格納部118とを有する。未解釈関数割当部106は、元制約データ格納部103と型情報格納部104と制約語彙定義格納部105とに格納されているデータを用いて処理を行い、第1データ格納部107に処理結果を格納する。制約変換部108は、型情報格納部104と第1データ格納部107と元制約データ格納部103とに格納されているデータを用いて処理を行い、第2データ格納部109に処理結果を格納する。SMTソルバインタフェース部110は、第2データ格納部109に格納されているデータをSMTソルバ200に出力し、SMTソルバ200から受け取った処理結果を第3データ格納部111に格納する。また、SMTソルバインタフェース部110は、第5データ格納部115に格納されているデータをSMTソルバ200に出力し、SMTソルバ200から受け取った処理結果については第6データ格納部116に格納する。充足値反映部112は、元制約データ格納部103と第1データ格納部107と第3データ格納部111とに格納されているデータを用いて処理を行い、処理結果を第4データ格納部113に格納する。制約構成部114は、第3データ格納部111と第4データ格納部113と制約語彙定義格納部105と元制約データ格納部103とに格納されているデータを用いて処理を行い、処理結果を第5データ格納部115に格納する。充足値変換部117は、第6データ格納部116に格納されているデータを用いて処理を行い、処理結果を第7データ格納部118に格納する。元制約データ格納部103には、例えば、図4に示されているような元制約データが格納されているものとする。また、型情報格納部104には、商品検索画面の画面定義データと、商品マスタテーブル及び在庫状況テーブルのテーブル定義データとが格納される。型情報格納部104には、例えば図7に示すような画面定義データが格納される。図7の例では、定義されている画面の名称商品検索画面と、入力欄の項目名商品名と、当該項目の型文字列と、桁数5とが定義されている。また、型情報格納部104には、例えば図8に示すようなテーブル定義データも格納されている。図8の例では、テーブル名と、テーブル毎に、テーブルに含まれるカラムとカラムの型及び桁と、が登録されるようになっている。さらに、制約語彙定義格納部105には、例えば図9に示すような制約語彙定義データが格納されている。図9の例では、元制約データで用いられているprefixの具体的な定義が規定されている。ここではXの文字数がYの文字数以上の場合語彙名prefix1と、Xの文字数がYの文字数未満の場合語彙名prefix2が規定されている。これらは、前方一致を規定している。また、SMTソルバ200は、述語論理式の充足可能性判定問題を解く機構であり、テストデータ生成装置100に含まれる場合もあれば、別装置にて実装される場合もある。SMTソルバ200は、Yiceshttpyicescslsricom、CVC3httpwwwcsnyueduacsyscvc3、Z3httpresearchmicrosoftcomenusumredmondprojectsz3などが既に実装されており、DanielKroeningetalDecisionProceduresAnAlgorithmicPointofViewISBN:9783540741046にも詳細が記載されているので、ここではこれ以上述べない。次に、図10乃至図38を用いてテストデータ生成装置100の処理内容について説明する。まず、未解釈関数割当部106は、元制約データ格納部103と型情報格納部104と制約語彙定義格納部105とに格納されているデータを用いて、未解釈関数割当処理を実施する図10:ステップS1。未解釈関数割当処理については、図11乃至図15を用いて説明する。未解釈関数割当部106は、制約語彙定義格納部105に格納されている制約語彙定義データに含まれている制約語彙定義のうち、未処理の制約語彙定義を1つ特定する図11:ステップS11。そして、未解釈関数割当部106は、表現抽出処理を実施するステップS13。表現抽出処理については、図12を用いて説明する。未解釈関数割当部106は、ステップS11で特定された制約語彙定義におけるシグニチャに合致する式を、元制約データ格納部103に格納されている元制約データから抽出する図12:ステップS31。例えば図9に示したprefix1がステップS11で特定されたものとする。そして、このprefix1のパターンにおける引数X及びYは共に文字列型であるから、図4に示されている元制約データから、prefix1のパターンと同じ表記prefixの式あって、引数が共に文字列型となっている式を抽出する。この場合、型情報格納部104に格納されているデータから、画面定義における商品名の型が文字列であり、商品マスタテーブルの商品カラムの型が文字列であることが分かる。そうすると、prefix1のパターンのシグニチャに合致すると判断できるので、prefix、prefix及びprefixが抽出される。そして、未解釈関数割当部106は、ステップS31で式が抽出されたか確認するステップS33。抽出されない場合には元の処理に戻る。一方、ステップS31で式が抽出された場合には、未解釈関数割当部106は、抽出された式のうち未処理の式を1つ特定するステップS35。そして、未解釈関数割当部106は、特定された抽出式の引数と制約語彙定義の条件とを比較するステップS37。図4に示されている元制約データから抽出されたprefixが、特定された制約語彙定義prefix1の条件に合致するか否かは、型情報格納部104に格納されているデータを基に判断する。具体的には、画面定義における商品名の桁数は文字列5であり、商品マスタテーブルの商品カラムの桁数は文字列5であるから、特定された制約語彙定義の条件maxlengthの引数は、特定された制約語彙定義の条件を満たしていると判断される。条件を満たしていない場合にはステップS43に移行する。一方、条件を満たしている場合には、未解釈関数割当部106は、特定された抽出式を表現抽出リストに追加するステップS41。そして、未解釈関数割当部106は、未処理の抽出式が存在しているか判断しステップS43、未処理の抽出式が存在している場合にはステップS35に戻る。一方、未処理の抽出式が存在していない場合には、元の処理に戻る。図12の処理を図4に示した元制約データに対して行うと、表現抽出リストは図13に示すようなリストとなる。図11の処理の説明に戻って、未解釈関数割当部106は、元制約データに該当表現が存在するかを、表現抽出リストで判断するステップS15。表現抽出リストに式が登録されていない場合には、該当表現が存在しないと判断してステップS21に移行する。一方、表現リストに式が登録されている場合には、未解釈関数割当部106は、特定された制約語彙定義から、未解釈関数パターンを生成し、第1データ格納部107に格納するステップS17。例えば、本具体例では、図14に示すような未解釈関数パターンのデータが生成され、第1データ格納部107に格納される。図14の例では、パターンIDと、制約語彙定義におけるパターン又は語彙名と、当該パターンに割り当てられた未解釈関数とが登録されるようになっている。すなわち、ステップS17では、特定された制約語彙定義に対して、1つの未解釈関数を割り当てる。このような未解釈関数uninterpretedfunctionを導入することによって、SMTソルバ200は、具体的に制約語彙定義におけるパターンを制約として解くのではなく、他の制約を満たすように未解釈関数の入出力関係を特定するようになる。未解釈関数は、特定の入力に対する出力の対応関係のみで定義される関数であり、入力から出力を特定する対応表を表現しているともいえる。入力から出力を計算するロジックを無視して関数すなわち、ここでは制約を抽象化するために用いられる。例えば、整数xを入力として、整数を出力する未解釈関数ufuncを想定した場合、ufunc100である場合には、計算ロジックは不明でも、未解釈関数ufuncに対して10を入力すると100を出力する関数であると解釈される。ここで、funcxxである場合に、x=y且つfunc≠funcという制約が充足可能であるか判定することを想定する。この際、func≠funcについてfuncの定義をそのまま展開してxx≠yyとしなくても、funcの代わりに未解釈関数ufuncを代わりに用いてufunc≠ufuncとするだけでも充足不能であることを判定できる。funcの形が複雑であれば、未解釈関数ufuncを用いた方が充足不能であることを早期に判定できる可能性がある。未解釈関数は、このような数値型の変数だけではなく、文字列の変数にも適用できる。例えば、PA,Bを、整数Aと整数Bを入力として真偽trueorfalseを出力する未解釈関数とする。また、prefix且つSaSb且つprefixという制約の充足値を求めることを考える。このような場合にも、PA,Bという未解釈関数を導入すると共に、Sa,Sb,Sc,Sdの代わりにa,b,c,dといった整数型の代表値を導入する。そうすると、上で述べた制約はPa,bANDb=dANDPc,dという制約に書き換えられる。このような制約をSMTソルバ200に入力すると、a=100,b=200,c=100,d=200,P100,200は真trueという解が得られる。このような結果を得れば、prefixANDSbSdANDSaScというように制約が再構成されて、充足値SaScabcSbSdabcdが得られるようになる。このように、未解釈関数による抽象化は有用である。処理の説明に戻って、未解釈関数割当部106は、抽出された表現に対する未解釈関数割当情報を生成し、第1データ格納部107に格納するステップS19。例えば、本具体例では、図15に示すような未解釈関数割当情報が生成され、第1データ格納部107に格納される。図15の例では、割当IDと、抽出式と、パターンIDとが登録されるようになっている。このように、表現抽出リストに登録された式に対して、IDを割り当てると共に、未解釈関数パターンで割り当てられた該当パターンIDが対応付けられている。そして、未解釈関数割当部106は、制約語彙定義格納部105に登録されている制約語彙定義のうち、未処理の制約語彙定義が存在しているか判断しステップS21、未処理の制約語彙定義が存在している場合には、ステップS11に戻る。一方、未処理の制約語彙定義が存在していない場合には、元の処理に戻る。以上のような処理を実施することで、レコード単位制約に関連して定義されている制約語彙定義のパターン毎に、元制約データにおける当該パターンの出現形態が確認される。図10の処理の説明に戻って、制約変換部108は、第1データ格納部107と元制約データ格納部103とに格納されているデータを用いて、制約変換処理を実施するステップS3。この制約変換処理については、図16乃至図18を用いて説明する。まず、制約変換部108は、第1データ格納部107に格納されている未解釈関数割当情報における未処理のパターンを1つ特定する図16:ステップS51。そして、制約変換部108は、特定されたパターンに該当する式を元制約データから抽出しステップS53、抽出された式を、特定されたパターンに対応する未解釈関数で置換するステップS55。例えば図15の未解釈関数割当情報における最初のパターンを処理する場合には、図17に示すように、太線で囲まれた部分が抽出され、未解釈関数パターンに従って未解釈関数PX,Yで置換される。より具体的には、prefixについては、Pに置換される。未解釈関数割当情報の残りのパターンについても、同様に未解釈関数で置換される。そして、制約変換部108は、未処理のパターンが、未解釈関数割当情報に存在しているか確認するステップS57。未処理のパターンが未解釈関数割当情報に存在している場合にはステップS51に戻る。一方、未処理のパターンが存在しない場合には、図18に示すような処理後の制約データが生成されたことになる。図18の例では、prefix関数は用いられておらず、未解釈関数Pに置換されている。その後、制約変換部108は、処理後の元制約データの各文字列型変数を、数値型変数に置換して、この処理の後の元制約データを、レコード選択部分制約データとして、第2データ格納部109に格納するステップS59。そして元の処理に戻る。例えば、商品名商品マスタ.商品在庫状況.商品といった文字列型の変数については、同名の数値型変数に置換しておく。同名の数値型変数を置換することで、表記としては図18のデータはそのまま、レコード選択部分制約となる。このようにすれば、レコード単位制約を未解釈関数で置換して抽象化することで、レコード単位制約を同時に解くことがないように変換した制約データであるレコード選択部分制約が生成されたことになる。図10の処理の説明に戻って、SMTソルバインタフェース部110は、第2データ格納部109に格納されているレコード選択部分制約のデータを、SMTソルバ200に出力し、SMTソルバ200に、充足可能性判定処理を実施させるステップS5。SMTソルバ200は、レコード選択部分制約に対して充足可能性判定処理を実施して、充足可能であるならば充足値を算出し、SMTソルバインタフェース部110に出力する。SMTソルバインタフェース部110は、SMTソルバ200から、第1回目の処理結果を受け取り、第3データ格納部111に格納する。充足不能の場合には、充足不能を表すデータが第3データ格納部111に格納される。例えば充足値反映部112は、第3データ格納部111に格納されている、SMTソルバ200の第1回目の処理結果に充足値が含まれているか否かによって、レコード選択部分制約が充足可能であったか判断するステップS7。レコード選択部分制約が充足不能であった場合には、端子Bを介して処理を終了する。ユーザに対して充足不能を表すデータを出力するようにしてもよい。一方、SMTソルバ200の第1回目の処理結果に充足値が含まれている場合には、端子Aを介して、図23の処理に移行する。本具体例では、第1回目の処理結果として、第3データ格納部111に、図19乃至図22に示すようなデータが格納されるものとする。例えば、商品マスタテーブルのデータとして図19のようなデータがSMTソルバ200から得られる。図19の例では、商品名と単価の組み合わせが3つ含まれている。商品マスタ.商品は、上でも述べたように数値型変数に置換されているので、100200400といった数値になっている。単価については、非負の数値型変数のままである。また、在庫状況テーブルのデータとして図20のようなデータがSMTソルバ200から得られる。図20の例では、商品名と在庫数の組み合わせが2つ含まれている。在庫状況.商品は、上でも述べたように数値型変数に置換されているので、非負の数値型変数のままである。さらに、未解釈関数の入出力関係を表す未解釈関数入出力情報として図21に示すようなデータがSMTソルバ200から得られる。図21の例では、未解釈関数PX,YのX及びYに具体的な値を入れた場合に出力される論理値false又はtrueが示されている。ここでは300,100は偽falseであり、300,200は偽falseであり、300,400は真trueである。なお、X=300は、商品検索画面における商品名の値数値変数の値であり、模式的に示せば、テストデータとして、図22のような商品検索画面が想定される。すなわち、商品名の入力欄に、300という商品名に対応する値が設定される。このような第1回目の処理結果は、全体として、レコード単位制約の部分を除き元制約データについての制約を全て満たしている。すなわち、1入力された商品名に前方一致する商品が商品マスタテーブルにただ1件存在するという制約については、未解釈関数入出力情報から、入力された商品名300と商品マスタテーブルの商品名100との組み合わせについては偽、入力された商品名300と商品マスタテーブルの商品名200との組み合わせについては偽、入力された商品名300と商品マスタテーブルの商品名400については真とあるので、満たされている。但し、レコード単位制約についての前方一致については抽象化されている。さらに、2当該商品に対応する在庫状況テーブルの在庫数が1以上の場合、該当する商品の発注画面が表示されるという制約については、入力された商品名300と商品マスタテーブルの商品名400については真であるから、在庫状況テーブルにおける2番目のレコードから在庫数200が特定され、発注画面が表示されるので、満たされる。さらに、3商品マスタテーブルの全てのレコードに対して、商品が対応する在庫状況テーブルのレコードが0件又は1件存在するという制約については、商品マスタテーブルの商品名100200300に対して、在庫状況テーブルの商品名100400となっているので、満たされている。また、4在庫状況テーブルの全てのレコードに対して、商品が対応する商品マスタテーブルのレコードが1件存在するという制約についても、在庫状況テーブルの商品名は、商品マスタテーブルの商品名に全て存在しているので、満たされている。図23の処理の説明に移行して、充足値反映部112及び制約構成部114は、レコード単位部分制約生成処理を実施する図23:ステップS61。このレコード単位部分制約生成処理については、図24乃至図32を用いて説明する。まず、充足値反映部112は、第1データ格納部107と第3データ格納部111と元制約データ格納部103とに格納されているデータを用いて、割当関数入出力情報生成処理を実施する図24:ステップS71。割当関数入出力情報生成処理については、図25乃至図27を用いて説明する。まず、充足値反映部112は、第1データ格納部107に格納されている未解釈関数割当情報における未処理の制約を1つ特定する図25:ステップS81。例えば、未解釈関数割当情報図15における最初の制約prefixが特定された場合を想定する。そして、充足値反映部112は、特定された制約に対応する未解釈割当関数を、パターンIDを用いて未解釈関数パターン情報図14から特定するステップS83。本具体例では未解釈割当関数PX,Yしか存在しないが、複数ある場合にはその中からパターンIDで特定する。その後、充足値反映部112は、特定された制約で利用されている変数の値を、第3データ格納部111に格納されている第1回目の処理結果から特定し、対応する未解釈関数の値を取得するステップS85。prefixの場合には、入力される商品名は第1回目の処理結果図22から300と特定され図261、商品マスタ0商品についても第1回目の処理結果図19から100と特定される図262。そして、未解釈関数パターン情報図14から、P300,100という未解釈関数が構成されるので図263乃至5、未解釈関数入出力情報図21の最初のレコードから、偽falseを変数値として特定する。そして、充足値反映部112は、ステップS81で特定された制約と、ステップS85で取得された当該パターンの値とを対応付けて割当関数入出力情報リストに登録するステップS87。その後、充足値反映部112は、第1データ格納部107に格納されている未解釈関数割当情報において未処理のパターンが存在するか判断するステップS89。未処理の制約が存在する場合には、ステップS81に戻る。一方、未処理の制約が存在しない場合には、元の処理に戻る。このような処理を実施すれば、図27に示すような割当関数入出力情報リストが生成されて、第4データ格納部113に格納される。図27の例では、パターン未解釈関数パターン情報におけるパターンと、元制約中の表現未解釈関数割当情報における制約と、値とが対応付けられている。このようにして、今回生成するテストデータに従って行われるテストにおいて、データベースのいずれのレコードが用いられるのかが明らかになる。図27の例では、prefixのみが真であるので、商品テーブルの3番目のレコードが抽出されることになる。図24の処理の説明に戻って、充足値反映部112は、代表値関係情報構成処理を実施するステップS73。この代表値関係情報構成処理については、図28乃至図30を用いて説明する。まず、充足値反映部112は、未解釈関数を割り当てられなかった変数間の関係式を、元制約データ格納部103に格納されている元制約データから抽出する図28:ステップS91。図4のような元制約データのうち、未解釈関数が割り当てられたのは、prefix関数が用いられている部分のみであるから、他の関係式が本ステップで抽出される。ステップS91では、図29のようなデータが抽出される。図29の例では、X=Yのパターンと、X≧Yのパターンが存在しており、それぞれに元制約中の表現パターンが抽出されて、登録されている。なお、X=YパターンのX及びYは文字列型の変数であるが、数値型の変数に変換して第1回目の充足可能性判定処理が実施されている。そして、充足値反映部112は、ステップS91で1つでも関係式が抽出されたか判断するステップS93。1つも関係式が抽出されていない場合には、これ以上処理を行わないので、元の処理に戻る。一方、1つでも関係式が抽出される場合には、充足値反映部112は、抽出された関係式のうち未処理の関係式を1つ特定するステップS95。次に、充足値反映部112は、特定された関係式が代表値関係情報に既に登録されているか判断するステップS97。特定された関係式が代表値関係情報に既に登録済みである場合には、ステップS103に移行する。一方、特定された関係式が未登録であれば、充足値反映部112は、特定された関係式内の変数に、第3データ格納部111に格納されている第1回目の処理結果に含まれる該当値を代入して、特定された関係式の結果を算出するステップS99。図29の第1行目を一例にすると、商品マスタ0商品=在庫状況0商品であるが、第1回目の処理結果からすると商品マスタ0商品の値は100で、在庫状況0商品の値は100であるので、関係式の結果は真trueとなる。そして、充足値反映部112は、特定された関係式及び算出された結果を、代表値関係情報に登録するステップS101。この代表値関係情報は、第4データ格納部113に格納される。その後、充足値反映部112は、未処理の関係式が存在するか判断しステップS103、未処理の関係式が存在する場合にはステップS95に戻る。一方、未処理の関係式が存在しない場合には、元の処理に戻る。このような処理を実施すれば、図30に示すような代表値関係情報が得られる。図30の例では、パターンと、元制約中表現の表現パターンと、値とが対応付けて登録されている。図24の処理に戻って、次に、制約構成部114は、第3データ格納部111と第4データ格納部113と元制約データ格納部103と制約語彙定義格納部105とに格納されているデータを用いて、レコード単位部分制約生成処理を実施するステップS75。このレコード単位部分制約生成処理については、図31及び図32を用いて説明する。まず、制約構成部114は、割当関数入出力情報図27において、未処理の表現パターンを1つ特定する図31:ステップS111。そして、制約構成部114は、特定された表現パターンについて、制約語彙定義から対応する条件を生成するステップS113。例えば、図27の第1行目のprefixについて処理する場合には、図9に示したprefix1のパターンに従って条件を生成する。具体的には、図5に示すような条件に展開する。このような展開については、従来技術と同様であるからここでは説明を省略する。そして、制約構成部114は、特定された表現パターンの値を、生成された条件の値として制約を生成し、連言で追加するANDで連結するステップS115。その後、制約構成部114は、未処理の表現パターンが割当関数入出力情報に存在しているか判断するステップS117。未処理の表現パターンが存在している場合にはステップS111に戻る。一方、未処理の表現パターンが存在しない場合には、代表値関係情報図30についての処理に移行する。なお、図27に示した割当関数入出力情報の場合、表現パターンprefixの値は偽falseであるから、notprefixとなる。また、表現パターンprefixの値も偽falseであるから、notprefixを、notprefixに対してANDで連結する。さらに、表現パターンprefixの値は真trueであるから、prefixをさらにANDで連結する。すなわち、図32において破線で囲まれた制約Aが形成される。但し、prefix関数の部分は、実際には図5のような形で展開されている。次に、制約構成部114は、代表値関係情報において、未処理の表現パターンを1つ特定するステップS119。そして、制約構成部114は、特定された表現パターンとその値とから制約を生成し、連言で追加するANDで連結するステップS121。図30の例では、表現パターン商品マスタ0商品=在庫状況0商品とその値真trueとから、商品マスタ0商品=在庫状況0商品という制約を生成し、ANDで連結する。また、表現パターン商品マスタ0商品=在庫状況1商品とその値偽falseとから、not商品マスタ0商品=在庫状況1商品という制約を生成し、ANDで連結する。その後、制約構成部114は、代表値関係情報に未処理の表現パターンが存在するか判断するステップS123。未処理の表現パターンが存在する場合にはステップS119に戻る。一方、未処理の表現パターンが存在しない場合には、第3データ格納部111に格納されている第1回目の処理結果のデータベースのデータのうち数値型変数の値についての制約を生成する処理に移行する。図30のような代表値関係情報の場合には、図32において一点鎖線で囲まれる制約Bが形成される。その後、制約構成部114は、データベースのデータのうち数値型変数とその値とを制約として生成し、連言で追加するANDで連結するステップS125。元々数値型変数というのは、在庫状況テーブルの在庫数及び商品マスタテーブルの単価であり、それらの値は図19及び図20に示すような値として算出されている。従って、在庫状況0在庫数=100、在庫状況1在庫数=200、商品マスタ0単価=1000、商品マスタ1単価=2000、商品マスタ2単価=3000という制約が生成され、ANDで連結される。そうすると、図32において点線で囲まれる制約Cが形成される。このような処理を実施することで、図32一部は図5のような制約で展開されているのような制約データがレコード単位部分制約として生成され、第5データ格納部115に格納される。図32に示したレコード単位部分制約は、図4に示した元制約を満たすことが確認された、レコード選択部分制約についての充足値で、元制約を間接的に反映させて、レコード単位制約のための制約として再構成したものである。すなわち、このようなレコード単位部分制約に充足値が存在する場合には、その充足値が元制約をも充足するように、レコード単位部分制約が生成されている。従って、一部はそのまま対応している部分はあるが、表現として図4と図32を比較することは意味がない。図23の処理の説明に戻って、SMTソルバインタフェース部110は、第5データ格納部115に格納されているレコード単位部分制約のデータを、SMTソルバ200に出力し、SMTソルバ200に、充足可能性判定処理を実施させるステップS63。SMTソルバ200は、レコード単位部分制約に対して充足可能性判定処理を実施して、充足可能であるならば充足値を算出し、SMTソルバインタフェース部110に出力する。SMTソルバインタフェース部110は、SMTソルバ200から、第2回目の処理結果を受け取り、第6データ格納部116に格納する。充足不能の場合には、充足不能を表すデータが第6データ格納部116に格納される。例えば充足値変換部117は、第6データ格納部116に格納されている、SMTソルバ200の第2回目の処理結果に充足値が含まれているか否かによって、レコード単位部分制約が充足可能であったか判断するステップS65。レコード単位部分制約が充足不能であった場合には、処理を終了する。ユーザに対して充足不能を表すデータを出力するようにしてもよい。一方、SMTソルバ200の第2回目の処理結果に充足値が含まれている場合には、例えば図33乃至図35のような処理結果が得られる。図33は、商品検索画面における商品名の値数値配列の値を模式的に示すものである。すなわち、テストデータとして、図33のような商品検索画面が想定され、数値配列の要素値が5つ65666700が得られる。また、図34に示すように、商品マスタテーブルの商品名に相当する数値配列の要素値が5つずつ得られる。図35にも、同様に在庫状況テーブルの商品名に相当する数値配列の要素値が5つずつ得られる。そうすると、充足値変換部117は、充足値を文字列に変換してテストデータを生成し、第7データ格納部118に格納するステップS67。具体的には、文字列変数を数値配列として取り扱った場合には、数値配列の要素値をそれぞれ文字に変換することで、文字列を得る。例えば、65などを、対応する文字コードに置換する。そうすると、図33における65666700は図36に示すように文字列ABCに変換される。同様に、図34の商品マスタテーブルの商品名についても、図37に示すようにAAAAAABBABCDという文字列に変換される。さらに、図35の在庫状況テーブルの商品名についても、図38に示すようにAAAAABCDという文字列に変換される。以上のような処理を実施することで、前方一致等の複雑な制約であっても、高速にテストデータを生成することができるようになる。なお、商品マスタテーブル及び在庫状況テーブルをそれぞれ10レコード含むテストデータを生成する場合、全ての制約を一度に解く場合に比して処理時間が約1/5になるという実験結果も得ている。以上本技術の実施の形態を説明したが、本技術はこれに限定されるものではない。例えば、機能ブロック図図6は一例であって必ずしも実際のプログラムモジュール構成とは一致しない場合もある。処理フローについても、処理結果が変わらない限り、処理順番を入れ替えたり、並列実行できる場合がある。さらに、上では前方一致という制約を問題としていたが、部分一致その他の複雑な制約も取り扱うことができる。さらに、未解釈関数で抽象化する関数の一例として、前方一致の関数prefixが語彙定義情報に含まれている例を示したが、レコード単位制約が特定できれば、どのような形で規定されていても良い。さらに、元制約データを生成する処理部が、テストデータ生成装置100に含まれる場合もある。さらに、SMTソルバ200の機能と、テストデータ生成装置100の機能とが一体となって、頒布される場合もある。また、レコード単位部分制約を生成する際に、第1回目の処理結果に含まれる数値型変数についての処理結果についてはそのまま制約に用いているが、文字列型に関しては、その代表値の大小関係を辞書順と解釈して順序関係の制約をつけてもよい。なお、上で述べたテストデータ生成装置100は、コンピュータ装置であって、図39に示すように、メモリ2501とCPUCentralProcessingUnit2503とハードディスクドライブHDD:HardDiskDrive2505と表示装置2509に接続される表示制御部2507とリムーバブルディスク2511用のドライブ装置2513と入力装置2515とネットワークに接続するための通信制御部2517とがバス2519で接続されている。オペレーティングシステムOS:OperatingSystem及び本実施例における処理を実施するためのアプリケーションプログラムは、HDD2505に格納されており、CPU2503により実行される際にはHDD2505からメモリ2501に読み出される。CPU2503は、アプリケーションプログラムの処理内容に応じて表示制御部2507、通信制御部2517、ドライブ装置2513を制御して、所定の動作を行わせる。また、処理途中のデータについては、主としてメモリ2501に格納されるが、HDD2505に格納されるようにしてもよい。本技術の実施例では、上で述べた処理を実施するためのアプリケーションプログラムはコンピュータ読み取り可能なリムーバブルディスク2511に格納されて頒布され、ドライブ装置2513からHDD2505にインストールされる。インターネットなどのネットワーク及び通信制御部2517を経由して、HDD2505にインストールされる場合もある。このようなコンピュータ装置は、上で述べたCPU2503、メモリ2501などのハードウエアとOS及びアプリケーションプログラムなどのプログラムとが有機的に協働することにより、上で述べたような各種機能を実現する。以上述べた本実施の形態をまとめると、以下のようになる。本テストデータ生成方法は、Aプログラムのテストに用いられるデータベース内のテストデータについての制約を表す第1の制約データを格納する第1データ格納部に格納されている第1の制約データにおいて、テストデータに含まれるべきレコードの選択に関する制約であるレコード選択制約に従って選択したレコードが満たすべき制約であるレコード単位制約についての第1の表現パターンを、未解釈関数で置換することによって第2の制約データを生成し、第2データ格納部に格納する第1制約生成ステップと、B第2データ格納部に格納されている第2の制約データに対して充足可能性判定処理を実施させ、第1の制約データについての第1の充足値を取得し、第3データ格納部に格納するステップと、C第3データ格納部に格納されている第1の充足値と、第1の制約データに含まれる第1の表現パターンと、第1の制約データに含まれる、第1の表現パターン以外の制約についての第2の表現パターンとから、レコード単位制約についての第3の制約データを生成し、第4データ格納部に格納する第2制約生成ステップと、D第4データ格納部に格納されている第3の制約データに対して充足可能性判定処理を実施させ、前記第3の制約データについての第2の充足値を取得し、第4データ格納部に格納するステップとを含む。このように2段階に分けて充足可能性判定処理を実施させるので、それぞれについて処理すべき制約が単純化され、個別の判定処理及び全体の処理が高速化される。また、文字列変数を数値型の変数に変換しておき、上記方法において、第4データ格納部に格納されている第2の充足値に含まれる、数値型の変数の値を、文字列に変換するステップをさらに含むようにしても良い。このようにすれば文字列変数についても高速に処理できる。さらに、上で述べた第2制約生成ステップが、C1第1の充足値に含まれる未解釈関数の入出力対応データから、第1の表現パターンの各々の真偽を特定し、第1の表現パターンの各々と対応する真偽との組み合わせについての制約を生成する第1生成ステップと、C2第1の充足値から、第2の表現パターンの各々の真偽を特定し、第2の表現パターンの各々と対応する真偽との組み合わせについての制約を生成する第1生成ステップと、C3第1の充足値に含まれるデータベース内の各レコードの値を表す制約と、第1生成ステップ及び第2生成ステップで生成された制約とを含む制約データを生成するステップとを含むようにしてもよい。これによって、元制約を間接的に反映させたレコード単位制約についての制約を生成することができる。また、上で述べた第1生成ステップが、第1の表現パターンの各々と対応する真偽との組み合わせについての制約を、第1の表現パターンに関連する制約定義に従って展開するステップをさらに含むようにしてもよい。適切な第3の制約データを生成することができる。なお、上で述べたような処理をコンピュータに実施させるためのプログラムを作成することができ、当該プログラムは、例えばフレキシブルディスク、CD-ROMなどの光ディスク、光磁気ディスク、半導体メモリ例えばROM、ハードディスク等のコンピュータ読み取り可能な記憶媒体又は記憶装置に格納される。なお、処理途中のデータについては、RAM等の記憶装置に一時保管される。以上の実施例を含む実施形態に関し、さらに以下の付記を開示する。付記1プログラムのテストに用いられるデータベース内のテストデータについての制約を表す第1の制約データを格納する第1データ格納部に格納されている前記第1の制約データに含まれる、前記テストデータに含まれるべきレコードの選択に関する制約であるレコード選択制約に従って選択したレコードが満たすべき制約であるレコード単位制約についての第1の表現パターンを、未解釈関数で置換することによって第2の制約データを生成し、第2データ格納部に格納する第1制約生成ステップと、前記第2データ格納部に格納されている前記第2の制約データに対する充足可能性判定処理を充足可能性判定処理部に実施させ、前記第1の制約データについての第1の充足値を前記充足可能性判定処理部から取得し、第3データ格納部に格納するステップと、前記第3データ格納部に格納されている前記第1の充足値と、前記第1の制約データに含まれる第1の表現パターンと、前記第1の制約データに含まれる、前記第1の表現パターン以外の制約についての第2の表現パターンとから、前記レコード単位制約についての第3の制約データを生成し、第4データ格納部に格納する第2制約生成ステップと、前記第4データ格納部に格納されている前記第3の制約データに対する充足可能性判定処理を充足可能性判定処理部に実施させ、前記第3の制約データについての第2の充足値を前記充足可能性判定処理部から取得し、第4データ格納部に格納するステップと、を、コンピュータに実行させるためのテストデータ生成プログラム。付記2前記第1の制約データに含まれる文字列変数を数値型の変数に変換する変換ステップと、前記第4データ格納部に格納されている前記第2の充足値に含まれ且つ前記変換ステップで変換された、前記数値型の変数の値を、文字列に変換するステップと、を、さらに前記コンピュータに実行させるための付記1記載のテストデータ生成プログラム。付記3前記第2制約生成ステップが、前記第1の充足値に含まれる前記未解釈関数の入出力対応データから、前記第1の表現パターンの各々の真偽を特定し、前記第1の表現パターンの各々と対応する真偽との組み合わせについての制約を生成する第1生成ステップと、前記第1の充足値から、前記第2の表現パターンの各々の真偽を特定し、前記第2の表現パターンの各々と対応する真偽との組み合わせについての制約を生成する第1生成ステップと、前記第1の充足値に含まれる前記データベース内の各レコードの値を表す制約と、前記第1生成ステップ及び前記第2生成ステップで生成された制約とを含む制約データを生成するステップと、を含む付記1又は2記載のテストデータ生成プログラム。付記4前記第1生成ステップが、前記第1の表現パターンの各々と対応する真偽との組み合わせについての制約を、第1の表現パターンに関連する制約定義に従って展開するステップをさらに含む付記3記載のテストデータ生成プログラム。付記5プログラムのテストに用いられるデータベース内のテストデータについての制約を表す第1の制約データを格納する第1データ格納部に格納されている前記第1の制約データにおいて、前記テストデータに含まれるべきレコードの選択に関する制約であるレコード選択制約に従って選択したレコードが満たすべき制約であるレコード単位制約についての第1の表現パターンを、未解釈関数で置換することによって第2の制約データを生成し、第2データ格納部に格納する第1制約生成ステップと、前記第2データ格納部に格納されている前記第2の制約データに対して充足可能性判定処理を実施し、前記第1の制約データについての第1の充足値を取得し、第3データ格納部に格納するステップと、前記第3データ格納部に格納されている前記第1の充足値と、前記第1の制約データに含まれる第1の表現パターンと、前記第1の制約データに含まれる、前記第1の表現パターン以外の制約についての第2の表現パターンとから、前記レコード単位制約についての第3の制約データを生成し、第4データ格納部に格納する第2制約生成ステップと、前記第4データ格納部に格納されている前記第3の制約データに対して充足可能性判定処理を実施し、前記第3の制約データについての第2の充足値を取得し、第4データ格納部に格納するステップと、を含み、コンピュータにより実行されるテストデータ生成方法。付記6プログラムのテストに用いられるデータベース内のテストデータについての制約を表す第1の制約データを格納する第1データ格納部に格納されている前記第1の制約データにおいて、前記テストデータに含まれるべきレコードの選択に関する制約であるレコード選択制約に従って選択したレコードが満たすべき制約であるレコード単位制約についての第1の表現パターンを、未解釈関数で置換することによって第2の制約データを生成し、第2データ格納部に格納する手段と、充足可能性判定処理部と、前記第2データ格納部に格納されている前記第2の制約データに対して充足可能性判定処理を前記充足可能性判定処理部に実施させ、前記第1の制約データについての第1の充足値を前記充足可能性判定処理部から取得し、第3データ格納部に格納する処理手段と、前記第3データ格納部に格納されている前記第1の充足値と、前記第1の制約データに含まれる第1の表現パターンと、前記第1の制約データに含まれる、前記第1の表現パターン以外の制約についての第2の表現パターンとから、前記レコード単位制約についての第3の制約データを生成し、第4データ格納部に格納する手段と、を有し、前記処理手段は、前記第4データ格納部に格納されている前記第3の制約データに対して充足可能性判定処理を前記充足可能性判定処理部に実施させ、前記第3の制約データについての第2の充足値を前記充足可能性判定処理部から取得し、第4データ格納部に格納する、テストデータ生成装置。"