"プログラムモデル検査装置用のDBシーケンスバックトラック制御プログラムであって、アプリケーションプログラムからのDB操作コマンドのシーケンス番号取得要求に応答して、DBMSに代わってシーケンス番号を出力することによって前記シーケンス番号取得要求の存在しないDB操作コマンドを前記DBMSに伝達すると共に前記シーケンス番号の状態の履歴を前記アプリケーションプログラムの状態と対応付けて記憶部に記憶し、前記プログラムモデル検査装置により指定されたアプリケーションプログラムの状態まで戻すバックトラック要求に応答して、前記記憶部に記憶された前記シーケンス番号の状態の履歴に基づいて、前記シーケンス番号の状態を、前記指定されたアプリケーションプログラムの状態と対応する状態までバックトラックさせる、処理をコンピュータに実行させることを特徴とするプログラム。前記記憶部に記憶する処理は、アプリケーションプログラムからのDB操作コマンドを、シーケンス番号取得要求に係るDB操作コマンドと、その他のDB操作コマンドとに分離し、前記シーケンス番号取得要求に係るDB操作コマンドから、シーケンス番号取得要求を抽出し、前記抽出されたシーケンス番号取得要求に応答して、DBMSに代わって前記シーケンス番号を出力することによりシーケンス番号の状態の履歴をアプリケーションプログラムの状態と対応付けて記憶部に保存し、前記シーケンス番号取得要求に係るDB操作コマンドのうち、シーケンス番号取得要求が組み込まれたDB操作コマンドの中の前記組み込まれたシーケンス番号取得要求を、前記出力されたシーケンス番号に置換したDB操作コマンドと、前記その他のDB操作コマンドと、を前記DBMSに伝達する、処理を有することを特徴とする請求項2記載のプログラム。プログラムモデル検査装置用のDBシーケンスバックトラック制御方法であって、アプリケーションプログラムからのDB操作コマンドのシーケンス番号取得要求に応答して、DBMSに代わってシーケンス番号を出力することによって前記シーケンス番号取得要求の存在しないDB操作コマンドを前記DBMSに伝達すると共に前記シーケンス番号の状態の履歴を前記アプリケーションプログラムの状態と対応付けて記憶部に記憶し、前記プログラムモデル検査装置により指定されたアプリケーションプログラムの状態まで戻すバックトラック要求に応答して、前記記憶部に記憶されたシーケンス番号の状態の履歴に基づいて、前記シーケンス番号の状態を、前記指定されたアプリケーションプログラムの状態と対応する状態までバックトラックさせる、ことを特徴とする方法。プログラムモデル検査装置用のDBシーケンスバックトラック制御装置であって、アプリケーションプログラムからのDB操作コマンドのシーケンス番号取得要求に応答して、DBMSに代わってシーケンス番号を出力することによって前記シーケンス番号取得要求の存在しないDB操作コマンドを前記DBMSに伝達すると共に前記シーケンス番号の状態の履歴を前記アプリケーションプログラムの状態と対応付けて記憶部に記憶する、シーケンス番号処理部と、前記プログラムモデル検査装置により指定されたアプリケーションプログラムの状態まで戻すバックトラック要求に応答して、前記記憶部に記憶されたシーケンス番号の状態の履歴に基づいて、前記シーケンス番号の状態を、前記指定されたアプリケーションプログラムの状態と対応する状態までバックトラックさせる、シーケンスバックトラック部と、を有することを特徴とする装置。本プログラム、方法、及び装置は、上記実情に鑑みなされたものであり、DBを利用するアプリケーションプログラムを検査対象とするプログラムモデル検査において、DBのシーケンス処理をも含めてバックトラックできる改善された技術を提供することを目的とする。本プログラムの一観点によれば、プログラムモデル検査装置用のDBシーケンスバックトラック制御プログラムであって、アプリケーションプログラムからのDB操作コマンドのシーケンス番号取得要求に応答して、DBMSに代わってシーケンス番号を出力することによって前記シーケンス番号取得要求の存在しないDB操作コマンドを前記DBMSに伝達すると共に前記シーケンス番号の状態の履歴を前記アプリケーションプログラムの状態と対応付けて記憶部に記憶し、前記プログラムモデル検査装置により指定されたアプリケーションプログラムの状態まで戻すバックトラック要求に応答して、前記記憶部に記憶された前記シーケンス番号の状態の履歴に基づいて、前記シーケンス番号の状態を、前記指定されたアプリケーションプログラムの状態と対応する状態までバックトラックさせる、処理をコンピュータに実行させることを特徴とするプログラムが提供される。開示のプログラム、方法、及び装置によれば、DBMSのシーケンス機能を用いたアプリケーションプログラムに対しても、シーケンス番号のバックトラックが可能であり、モデル検査を実施することができる。図1は、本発明の一実施例としてのDBシーケンスバックトラック制御装置103が組み込まれたプログラムモデル検査を実行する装置101のブロック図である。図1において、プログラムモデル検査を実行する装置101は、DBMSを利用するモデル検査装置102と、一実施形態であるDBシーケンスバックトラック制御装置103と、検査対象プログラム104と、DBMS105を含んでいる。利用者は、装置101の入出力装置不図示を介して、DBMSを利用したアプリケーションプログラムのプログラムモデル検査を実行することができる。装置101は、一台のコンピュータ上に実現しても良いし、あるいは、例えば、DBMSを別のコンピュータに配置することによって、複数台のコンピュータを用いて実現してもよい。DBMSを利用するモデル検査装置102と、一実施形態であるDBシーケンスバックトラック制御装置103と、検査対象プログラム104と、DBMS105は、CPUCentralProcessingUnitやプログラマブルなデバイスFPGAFieldProgrammableGateArray、PLDProgrammableLogicDeviceなど機器に実装されたプログラムとして実現できる。また、種々のデータやプログラムは、例えばROMReadOnlyMemory、RAMRandomAccessMemory、ハードディスクなどのメモリに記憶されてもよい。[シーケンス番号を利用するアプリケーションプログラムの例]ここでDBMSのシーケンス機能により、シーケンス番号を利用するアプリケーションプログラムの例を示す。図2は、商品購入Webアプリケーションの画面遷移の例を示す。選択画面210において、発注ボタン211と注文ボタン212が表示されている。発注の場合には、発注ボタン211をマウスでクリックすると、注文画面220が表示される。ここで、必要な注文内容を入力し、注文ボタン221をクリックする。画面は、完了画面230に移る。この段階で、データベース不図示にデータが格納され、注文No232として1が表示され、先ほど入力した注文内容が表示される。また、選択画面210において、注文検索ボタン212をクリックした場合には、検索画面240、検索結果画面250と遷移する。このように、データベースを用いるアプリケーションプログラムの場合には、注文No232のように、アプリケーション側がユニークな番号を自動的に付与して、注文の内容が一意に特定できるようになっている。図3は、データベース内のデータの例を示す図である。注文画面310にて注文内容を入力すると、アプリケーションプログラム320は、1注文情報を取得する。2DBMS330内の商品テーブル332に格納されている商品を確認する。3DBMSから、新たな注文Noを取得するためにシーケンス番号336として、次値の値である2を取得する。4次にDBMS330内の注文テーブル334内に新たなレコードとして、注文No335の欄に2を記入し、新たな注文データをINSERTし、格納する。このように、注文テーブル334内においては、注文No335が、注文のレコードを一意に特定するための主キーとして機能していることが分かる。また、アプリケーションプログラム320は、ユニークな注文NoをDBMSからシーケンス番号として取得していることが分かる。図4は、注文受付処理の前後のDBの状態を示している。DBMS410は、注文受付前のDBの状態を示している。DBMS420は注文受付後のDBMSの状態を示している。注文受付後においては、注文テーブル424にNo2のレコードが追加されている。また、シーケンス番号の注文Noの現在428の値が2に変化しているのが分かる。図5は、注文受付処理で発行されるSQLの例を示している。4つのSQLコマンドが列記されている。このうち、No.3のSELECT注文No.NEXTVALASSEQ_NEXTVALFROMDUALには、注文No.NEXTVALがふくまれており、注文Noとして、次のシーケンス番号を取得するコマンドを意味している。図6は、シーケンス番号生成用のDB操作コマンドの例を示している。シーケンス番号の名前として、注文Noが定義されており、増分1、初期値0、最大値1000が指定されている。このシーケンス番号は、新しい値を取得する毎に、1ずつ増加する。そして、シーケンス番号を逆戻りさせるコマンドは用意されていないDBMSが多い。このようなDBMSでは、後述するようにバックトラックの際に、シーケンス番号を逆戻りさせることができないために、不都合が生じる。図7は、アプリケーションプログラムの状態遷移の例を示す。以下のように、一連の操作をシナリオとして予め用意しておき、シナリオに沿ってアプリケーションプログラムを実行させる。1選択画面、発注ボタン2注文画面、注文ボタン、顧客名:富士太郎、商品名:商品A、数量:103完了画面、戻るボタン4選択画面、発注ボタン5注文画面、注文ボタン顧客名:富士次郎商品名:商品B、数量:206完了画面、戻るボタン7選択画面、注文検索ボタン8検索画面、検索ボタン、顧客名:富士、注文No:19検索結果画面、戻るボタン図7には、一連のシナリオ操作1乃至9を行った際のデータベースの内容710乃至734及び状態初期状態、状態1、状態2が、対応付けて示されている。単純化するために、状態として、DB状態だけを示している。図7における具体的な状態遷移は以下のようになる。<状態遷移>操作1:選択画面で、発注ボタンを押下すると、注文画面に遷移する。初期状態からDBデータは変化しないので、状態は変化しない。操作2:注文画面で、顧客名に富士太郎、商品名に商品A、数量に10を入力して、注文ボタンを押下する。注文受付処理が動作して、商品テーブルの在庫数が更新され、注文Noシーケンスから注文Noが採番され注文Noは一つ増加する注文テーブルに注文情報が追加される。DBデータが変化したので、初期状態から状態1となる。操作3:完了画面で、戻るボタンを押下する。選択画面に戻る。DBは更新されないので、状態1から変化しない。操作4:選択画面で、発注ボタンを押下すると、注文画面に遷移する。DBデータは変化しないので、状態1のままである。操作5:注文画面で、顧客名に富士次郎、商品名に商品B、数量に20を入力して、注文ボタンを押下する。注文受付処理が動作して、商品テーブルの在庫数が更新され、注文Noシーケンスから注文Noが採番され注文Noは一つ増加する、注文テーブルに注文情報が追加される。DBデータが変化するので、状態1から状態2となる。操作6:完了画面で、戻るボタンを押下して、選択画面に戻る。DBは更新されないので、状態1から変化しない。操作7:選択画面で、注文検索ボタンを押下して、検索画面に遷移する。DBは変化しないので、状態2のままである。操作8:検索画面で、顧客名に富士、注文Noに1を入力して、検索ボタンを押下する。検索結果画面に遷移する。DBデータの参照だけであり、DBは変化しないので、状態2から遷移しない。操作9:検索結果画面で、戻るボタンを押下して、選択画面に戻る。上記操作9が終了した段階で、図7のシナリオでは、全ての操作で回数制限に達し、選択可能な操作が無くなる。このため、上記操作9の終了後、バックトラックが行われる。なお、上記シナリオは、注文1注文データ1で注文、注文2注文データ2で注文、検索1検索データ1で検索の操作を順に行ったものに該当する。<状態のバックトラック>上記操作9の後、状態2において、シナリオから選択可能な操作が無くなる。このため、プログラムモデル検査装置は、別のシナリオで検査を続行するため、選択可能な操作が存在する、操作3の実行後までバックトラックする。別のシナリオの例は、例えば、注文1、検索、注文2の操作である。図8は、状態バックトラックの例を示している。プログラムモデル検査装置は、別のシナリオで検査を続行するため、選択可能な操作が存在する操作3の実行直後までバックトラックする。データベースのバックトラックの際には、データ自体と、シーケンス番号との両者を元に戻さなければならない。従って、DBMSの内容は、本発明の実施形態では、図8のDBMSの状態710に戻すことができる。参考のために、本実施形態を用いない場合のDBMSの状態810を示す。この場合には、シーケンス番号である注文No814の値が2となっており、状態1における正しい値1を示していない。これは、DBMSにおいてシーケンス番号を逆戻りさせることができないために生じた不都合である。本実施形態では、この不都合を回避していることがわかる。なお、本実施形態の詳細については、以下の実施例の項において説明する。図9は、本発明の一実施形態としてのDBシーケンスバックトラック制御装置のブロック図を示している。なお、図9では、DBシーケンスバックトラック制御装置900に加えて、DMBS940を利用するプログラムモデル検査装置950、検査対象アプリケーションプログラム930、及びDBMS940も併せて示されており、相互の関係が把握できるようになっている。まず、DBシーケンスバックトラック制御装置900について説明する。DBシーケンスバックトラック制御装置900は、検査対象アプリケーションプログラム930からDBMS940に向けて送出されるDB操作コマンドを受信する。DB操作コマンドは、まず、DB操作コマンド解析分離部912に入力される。ここでは、DB操作コマンドが解析され、まず、シーケンス処理に係るDB操作コマンドと、その他のDB操作コマンドとに分離する。そして、シーケンス処理のDB操作コマンドから、シーケンス番号取得要求を抽出する。抽出されたシーケンス番号取得要求は、シーケンス管理部914に伝達される。そして、シーケンス番号取得要求が組み込まれたDB操作コマンドにはYESのマーキングを行う。このマーキングの処理については、図15を用いて後述する。そして、上述のその他のDB操作コマンドと、YESのマーキングされたDB操作コマンドは、DB操作コマンド置換部916に伝達される。すなわち、シーケンス処理のDB操作コマンドのうち、シーケンス番号取得要求が組み込まれたDB操作コマンド以外のDB操作コマンドは、DB操作コマンド置換部916に伝達されないシーケンス管理部914は、シーケンス番号取得要求を受け取り、DMBS940に代わってシーケンス番号を生成し、出力する。シーケンス状態の履歴をアプリケーションプログラムの状態と対応付けて保存する。アプリケーションプログラムの状態は、DMBS940を利用するプログラムモデル検査装置950から、状態IDとして提供される。また、シーケンスバックトラック部920からの指示に基づいて、バックトラックしたシーケンス状態を状態収集部956に伝達する。また、DB操作コマンド置換部に、DB操作コマンドの置換を行うためのシーケンス番号を伝達する。DB操作コマンド置換部916は、DB操作コマンド解析分離部からのDB操作コマンドを受け取り、YESにマーキングされたDB操作コマンドである場合には、そのDB操作コマンドの中のシーケンス番号取得要求を、シーケンス管理部から出力されたシーケンス番号に置換する。そして、DB操作コマンドをDMBS940に転送する。以上の操作によって、DBMS940には、シーケンス番号取得要求の存在しないDB操作コマンドが伝達されることになる。シーケンスバックトラック部920は、DBバックトラック部958によって指定されたアプリケーションプログラムの状態まで戻すバックトラック要求に応答して、シーケンス状態の履歴に基づいて、シーケンス状態を指定されたアプリケーションプログラムの状態と対応する状態までバックトラックさせる。上述の一連の処理によって、DB操作コマンド置換部916からDBMS940に転送されるDB操作コマンドの中には、シーケンス番号取得に関連する要求又はコマンドが取り除かれることとなる。このことは、DBMS940のシーケンス機能を用いないことになる。このため、シーケンス取得に関連する要求又はコマンドに対しては、DBMS940に代わって、シーケンス管理部914が処理を行うこととなる。そして、シーケンス番号の逆戻りもシーケンス管理部914の管理する履歴を使うこととなるため、シーケンス状態のバックトラックが実現できることになる。なお、シーケンス管理部914と、DB操作コマンド解析分離部912と、DB操作コマンド置換部916とは、連携して、シーケンス番号処理部910を形成している。このシーケンス番号処理部910は、以下の処理を行っている。すなわち、アプリケーションプログラムからDMBS940に向けて発せられたDB操作コマンドを受け取り、DB操作コマンドのシーケンス番号取得要求に基づいて、DMBS940に代わってシーケンス番号を生成し、シーケンス番号取得要求の存在しないDB操作コマンドをDMBS940に伝達し、シーケンス状態の履歴をアプリケーションプログラムの状態と対応付けて記録することである。次に、DMBS940を利用するプログラムモデル検査装置950について説明する。ドライバ953は、予め定められた一連の操作を記憶したシナリオに基づいて、検査対象アプリケーションプログラム930に指示を与える。すなわち、通常はオペレータが行う操作を、オペレータに代わって、シナリオに基づいてドライバ953が行う。状態収集部956は、アプリケーションプログラムの状態や、シーケンス管理部からのシーケンス番号状態を収集して、状態管理部954に転送する。状態管理部954は、検査対象アプリケーションプログラム930の状態を監視し、状態が変化する場合には、状態IDを変更する。状態IDは、バックトラックの状態を特定する際に用いてもよい。また、状態管理部954は、アプリケーションの状態を評価器952に送る。評価器952は、状態管理部954から送られたアプリケーションプログラムの状態がプロパティ管理部951から提供されるプロパティを満足するかをチェックする。このチェックにおいて、状態がプロパティを満足すれば、アプリケーションプログラム930は、仕様を満足していることが分かる。この点については、既に説明したとおりである。バックトラック部955は、状態管理部954からの指示に基づいて、バックトラックを行うための制御を司る。バックトラックの指示をPGプログラム変数バックトラック部957とDBバックトラック部958に送る。PG変数バックトラック部957は、アプリケーションプログラム930の変数をバックトラックすべき状態まで戻す機能を果たす。DBバックトラック部958は、DBMS940に対して、データのバックトラックを指示する。これは、DBMS940に対して送った一連のDB操作コマンドの処理の逆の処理をDMBS940に指示することにより実現できる。加えて、シーケンスバックトラック部に、シーケンス番号をバックトラックさせる指示を行う。シーケンス状態は、DMBS940に代わって、DBシーケンスバックトラック部920及びシーケンス管理部914が管理しているため、DBMS940に何ら影響を与えずに、シーケンス状態のバックトラックを実現する。シーケンス番号のバックトラックについては、既に説明したとおりである。なお、DB接続切換部941は、モデル検査を行わない場合に、アプリケーションプログラム930とDBMS940とを直接接続するためのスイッチである。図10Aは、DBシーケンスバックトラック制御の処理フローを示している。ステップ1010において、アプリケーションプログラムからDMBS940に向けて発せられたDB操作コマンドを受け取り、DB操作コマンドのシーケンス番号取得要求に基づいて、DMBS940に代わってシーケンス番号を生成し、シーケンス番号取得要求の存在しないDB操作コマンドをDMBS940に伝達し、シーケンス状態の履歴をアプリケーションプログラムの状態と対応付けて記録する。ステップ1020において、プログラムモデル検査装置950により指定されたアプリケーションプログラムの状態まで戻すバックトラック要求に応答して、シーケンス状態の履歴に基づいて、シーケンス状態を指定されたアプリケーションプログラムの状態と対応する状態までバックトラックさせる。図10Bも、DBシーケンスバックトラック制御の処理フローを示している。ここでは、図10Aで示したステップ1010を実現する他の実施形態を示している。ステップ1012において、シーケンス処理に係るDB操作コマンドと、その他のDB操作コマンドとに分離し、シーケンス処理のDB操作コマンドから、シーケンス番号取得要求を抽出し、シーケンス番号取得要求が組み込まれたDB操作コマンドにはマーキングを行う。ステップ1014において、シーケンス番号取得要求を受け取り、DMBS940に代わってシーケンス番号を生成し、シーケンス状態の履歴をアプリケーションプログラムの状態と対応付けて保存する。ステップ1016において、その他のDB操作コマンドと、マーキングされたDB操作コマンドとを受け取り、マーキングされたDB操作コマンドの中のシーケンス番号取得要求を、生成されたシーケンス番号に置換した後に、受け取ったDB操作コマンドをDMBS940に転送する。ステップ1020については、図10Aにおいて説明したとおりである。図11は、プログラムモデル検査装置の処理フローを示している。ステップ1110において、シナリオ中に現在状態で選択可能な操作があるか判断される。この判断がYESであればステップ1120に進む。この判断がNOであればステップ1170に進む。ステップ1120において、ドライバが選択可能な操作で検査対象アプリケーションプログラムを駆動する。ステップ1130において、状態を収集し、状態を管理し、状態IDと関連付けてシーケンス状態が管理保持される。ステップ1140において、状態がプロパティを満足するかがチェックされ、アプリケーションプログラムの状態を評価する。ステップ1150において、プロパティが成立したかすなわち状態がプロパティを満足するかがチェックされる。この判断がYESであれば、ステップ1110に戻る。この判断がNoであれば、ステップ1160に進む。ステップ1160において、プロパティ不成立を報告する。この場合には、アプリケーションプログラムが仕様を満足していないことが分かる。ステップ1170において、バックトラック可能かが判断される。この判断がNoであれば終了する。この場合には、アプリケーションプログラムは、仕様を満足していることが判明する。この判断がYESであれば、ステップ1180に進む。ステップ1180では、バックトラックが行われる。どこまでバックトラックすべきかの判断は、上述の深さ優先探索法でシナリオをチェックすることによって判明する。なお、この点の具体例については、後述する。そして、以下のバックトラックを実施する。1アプリケーションプログラムの変数のバックトラック2DBバックトラックaDBのデータのバックトラックbシーケンス番号のバックトラック以上が、プログラムモデル検査装置950の処理フローである。図12は、DB操作コマンド解析分離部912のフロー図を示している。ステップ1210において、アプリケーションプログラムから、DMBS940に向けて発行されたDB操作コマンドを取得する。DB操作コマンドは、アプリケーションプログラムから順次発行されるため、DB操作コマンドを取得した都度、以下の処理を行えばよい。ステップ1220において、取得したDB操作コマンドを構文解析し、シーケンス処理の判定ルール1225に基づき、シーケンス番号の取得に関連する処理シーケンス処理かを判定する。シーケンス処理の判定ルールの例については、図13を用いて後述する。ステップ1230において、DB操作コマンドがシーケンス処理か否かが判定される。判定がYesであれば、ステップ1240に進む。判定がNoであれば、ステップ1270に進む。ステップ1240において、DB操作コマンドからシーケンス番号取得要求を抽出し、これをシーケンス管理部914に送る。シーケンス処理に関係するDB操作コマンドには、DB操作コマンド単独でシーケンス番号取得要求を行うものと、DB操作コマンド内に組み込まれた形でシーケンス番号取得要求を行うものとが存在する以後、このタイプのDB操作コマンドを組み込みという語を用いて説明する。これらの具体例については図14及び図15を用いて後述する。このステップでは、いずれのタイプのDB操作コマンドであっても、シーケンス番号取得要求を抽出して、シーケンス管理部914に送る。ステップ1250において、シーケンス処理が、組み込みか否かが判断される。この判断がYesであればステップ1260に進む。この判断がNoであればステップ1280に進む。ステップ1280において、このステップに進んだ場合には、取得したDB操作コマンドをDB操作コマンド置換部に伝達しない。なぜなら、このステップに到達した場合には、DB操作コマンドは、DBコマンド内にシーケンス番号取得要求が組み込まれていない、シーケンス番号取得のみのためのDB操作コマンドだからである。すなわち、シーケンス番号の取得の処理をDMBS940に要求しないため、DMBS940に伝送する必要はない。その代わり、本実施形態では、シーケンス管理部914が、DMBS940に代わってシーケンス番号取得要求の処理を行っている。ステップ1260において、当該DB操作コマンドの組込み欄にYESの印を付けて、DB操作コマンド置換部に伝達する。ここで、Yesの印を付けるのは、このDB操作コマンドが、シーケンス番号取得要求が組み込まれたものであるということを予めマーキングしておくためである。DB操作コマンド置換部916において、このDB操作コマンドの中のシーケンス番号取得要求の部分を、シーケンス管理部914が生成したシーケンス番号で置き換える。このようにすることによって、この置き換えられたDB操作コマンドをDMBS940に送った場合にも、DMBS940は、シーケンス番号取得要求が組み込まれていないDB操作コマンドとして処理を行うことができるのである。ステップ1270において、DB操作コマンドをDMBS940に伝送する。このステップに進んだ場合、DB操作コマンドは、シーケンス番号取得要求とは関係のないものであるため、DMBS940に処理させても、後のバックトラックが可能だからである。以上の処理によって、DMBS940には、シーケンス番号取得要求の含まれないDB操作コマンドが送られることとなる。そして、上述したようにシーケンス番号取得要求に対しては、DMBS940に代わって、シーケンス管理部914が処理を行う。図13は、シーケンス処理の判別ルールの例を示している。No.1及びNo.2は、シーケンス名に対応するシーケンス番号を取得する命令である。これらは、シーケンス番号取得要求を行う単独のコマンドであるため、シーケンス管理部914にシーケンス番号取得要求を送ればよい。そして、これらのDB操作コマンドは、DMBS940に送らないようにする。図13のNo.3及びNo.4のコマンドは、INSERT文であり、レコードを追加しつつ、データを追加する処理の中で、シーケンス番号取得要求を組み込んだものである。このようなシーケンス番号取得要求を組み込んだDB操作コマンドは、シーケンス番号取得要求部分だけを、シーケンス管理部914が生成したシーケンス番号で置き換えて、DB操作コマンドを修正した後にDMBS940に送ることが必要である。このようにすることによって、修正されたDB操作コマンドを受け取ったDMBS940に、シーケンス番号取得要求の部分の処理をおこなわせないことができる。上記以外のDB操作コマンドについては、シーケンス処理とは関係のないDB操作コマンドであると認識させる。図14は、DB操作コマンド解析分離部912の入力と出力の例を示している。そして、シーケンス処理が組み込まれていない場合を示している。検査対象アプリケーションプログラム930から表1410のDB操作コマンドが入力された。この一連のDB操作コマンドのうち、No3のDB操作コマンドSELECT注文No.NEXTVALASSEQ_NEXTVALFROMDUALは、注文No.のシーケンス番号の次の値を要求するものである。このDB操作コマンドは、シーケンス番号取得要求が組み込まれたコマンドではないため、テーブル1430の出力2に示すように、DB操作コマンド置換部916には、送らなくてよい。その代わり、テーブル1420に示すように、シーケンス番号取得要求として出力1注文No.NEXTVALをシーケンス管理部914に送り、シーケンス番号を生成させ、出力させる。また、表1430の組込みの欄にNOを追加する。NOの意味は、DB操作コマンド置換部において、置換処理が不要であることを意味する。NOの代わりに、ブランクとしておいてもよい。図15は、DB操作コマンド解析分離部912の別の入力と出力の例を示しており、シーケンス番号取得要求が、DB操作コマンドに組み込まれている場合の例を示している。表1510のNo.3のコマンドは、INSERTINTO商品テーブル注文No,顧客名,商品コード,数量VALUES注文No.NEXTVAL,富士次郎,Item2,20となっており、INSERT分の中に、注文No.NEXTVALという、シーケンス番号取得要求が組み込まれている。この場合には、表1520に示すように、出力1としてシーケンス番号取得要求注文No.NEXTVALをシーケンス管理部914に送り、シーケンス番号を生成させる。そして、表1530に示すように出力2として、DB操作コマンドの組込み欄にYESをマーキングして、出力2をDB操作コマンド置換部に送る。ここで、YESをマーキングする意味は、DB操作コマンド置換部において、該当するDB操作コマンド内のシーケンス番号取得要求を、シーケンス管理部914からのシーケンス番号で置換するための目印として利用する。なお、以上のようなYESNoのマーキングは、一例であり、DB操作コマンド置換部での置換処理が行える処理であれば、どのような処理であってもよいことはいうまでもない。図16は、DB操作コマンド置換部916のフローを示している。ステップ1610において、DB操作コマンド解析分離部912から、DB操作コマンドを取得する。ステップ1620において、DB操作コマンドにシーケンス番号取得要求が組み込まれているかシーケンス処理が組み込みか否かが判断される。この判断がYesであれば、ステップ1630に進む。また、この判断がNoであれば、ステップ1650に進む。この判断は、図16及び図17において示した実施形態の場合には、組込みの欄にYESが付されているか否かをチェックすることにより行うことができる。ステップ1630において、組み込まれたシーケンス番号取得要求に対応するシーケンス番号を、シーケンス管理部914から取得する。ステップ1640において、取得したDB操作コマンドに組み込まれたシーケンス番号取得要求の部分を、シーケンス番号で置き換える。ステップ1650において、取得したDB操作コマンドを、DMBS940に伝達する。以上の操作によって、シーケンス番号取得要求を含まないDB操作コマンドがDMBS940に送られることが保証される。図17は、DB操作コマンド置換部916の入力と出力の例を示している。これは、図15で示した例を用いている。表1710に示されているように、入力のうち、No.3のコマンドは、INSERTINTO商品テーブル注文No,顧客名,商品コード,数量VALUES注文No.NEXTVAL,富士次郎,Item2,20となっており、シーケンス番号取得要求が組み込まれている。このため、表1720のNo.3に示されるように、この中の注文No.NEXTVALを、シーケンス管理部714から出力されたシーケンス番号2で置換し、INSERTINTO商品テーブル注文No,顧客名,商品コード,数量VALUES2,富士次郎,Item2,20とする。この操作によって、DMBS940には、シーケンス番号取得要求の組み込まれていないINSERT文が送られることになる。図18は、シーケンス管理部914のデータ構造を示している。シーケンス管理部914は、シーケンス状態データ1810と、シーケンス状態スタックデータ1820とを有する。図19に、シーケンス状態データの例を示す。シーケンス状態データ1910は、現時点における複数のシーケンス名例えば、注文No商品Noの状態を示している。各シーケンス名の現在値及び次値が示されている。これらは、動的に変化して行く。初期値増分及び最大値は、シーケンス番号の定義の際に指定された値である。具体的な定義コマンドは、図6に示したとおりである。図20は、シーケンス状態スタックデータの例を示す。図19のシーケンスデータを、状態管理部954からの状態IDと関連付けてスタック状にメモリに記憶して行く。たとえば、表2010は、状態ID=状態2である場合のスタックデータを示している。状態を保存する場合には、新たなデータをプッシュする。バックトラックが指示された場合には、シーケンスバックトラック部920により、シーケンス状態スタックデータが、必要な回数だけポップされる。そして、トップの位置にあるシーケンス状態スタックデータが、バックトラック後におけるシーケンス状態となる。図21は、シーケンス管理部914の初期化フローを示している。ステップ2110において、シーケンス生成用のDB操作コマンドを受け取る。このコマンドの例は、図6に示されている。ステップ2120においてシーケンス管理914の管理データスタックを生成し、1番目のデータをPushする。現在のシーケンス状態が、状態IDとともにシーケンススタックデータのTopに置かれる。図22は、シーケンス管理部914の動作フローを示している。ステップ2210において、シーケンス番号取得要求か否かが判断される。この判断がYesであれば、ステップ2220に進む。この判断がNoであれば、ステップ2270に進む。ステップ2220において、シーケンス番号取得要求を受け取る。ステップ2230において、シーケンス番号取得要求の対象シーケンス名を特定する。シーケンスには、例えば図20においては、注文Noと商品Noの2つが存在する。このステップにおいて、シーケンス名が特定される。ステップ2240において、シーケンス番号取得要求が次値を要求しているか否かが判断される。シーケンス番号取得要求には、現在値を要求する場合と次値を要求する場合の2つが存在するため、このステップにおいて、このいずれであるかを特定する。この判断がYesであれば、ステップ2250に進む。この判断がNoであればステップ2260に進む。ステップ2250において、次値が要求されているため、シーケンス状態データから、当該シーケンスの増分に従って、現在値と次値を更新する。ステップ2260において、シーケンス番号を出力する。ステップ2270において、シーケンス状態スタックデータの更新要求か否かが判断される。判断がYesの場合には、ステップ2280に進む。判断がNoである場合には、終了する。ステップ2280において、このステップでは、状態の保存が要求されている場合であるため、プログラムモデル検査装置950から状態IDを取得する。ステップ2290において、シーケンス状態スタックデータに、状態IDとシーケンス状態データをまとめて、Pushする。図23は、シーケンス管理部914の管理データの変化の例を示している。まず、シーケンス管理部914の表2310はシーケンス状態を示しており、表2320は、シーケンス状態スタックデータを示している。この状態において、プログラムモデル検査装置950から、シーケンス状態スタックデータの更新が指示されたと仮定する。この場合には、新たな状態IDとして状態2が、プログラムモデル検査装置950から提供される。そして、シーケンス状態スタックデータが、表2340に示すように、状態2のエントリをプッシュして、更新される。このようにして、各々の状態IDと関連させてシーケンス状態がプッシュされる形で保存されて行く。図24は、シーケンスバックトラック部920のフローを示している。ステップ2410において、バックトラックすべき状態を取得し、バックトラック状態とする。ステップ2420において、シーケンス状態スタックデータに対して、バックトラック状態まで、スタックをPopする。このPop動作によって、適切なシーケンススタックデータがトップの位置に置かれることとなる。ステップ2430において、シーケンス状態スタックデータのTopから、シーケンス情報を取得して、シーケンス状態データとする。この操作によって、シーケンス状態は、バックトラックされ、シーケンス番号が逆戻りすることとなる。図25は、シーケンスバックトラックの例を示している。シーケンスバックトラック部920は、バックトラックすべき状態IDまで、シーケンス管理部914のシーケンス状態スタックデータに対して、スタックをPopする処理を行う。この図の例の場合には、状態1までバックトラックすることが示されている。したがって、シーケンス管理部914のシーケンス状態スタックデータのTopに状態1が来るよう、Popの操作がなされる。この状態が、表2520に示されている。図26は、操作シナリオの例を示している。シナリオには、シナリオNoが付されており。しなりおNo1を終了した後、順次次のシナリオを実行して行く。シナリオに基づいて、ドライバ953が、検査対象アプリケーションプログラム930を操作する。例えば、シナリオNo1が終了すると、次にシナリオNo2の実行が行われる。その際、シナリオNo2は、最初の1注文1から開始するのではなく、シナリオNo1の状態を1注文1の終了時点までバックトラックする。そして、ドライバは、シナリオ2の4検索の操作をアプリケーションプログラム930に対して行う。バックトラックの手法として、深さ優先探索法によって状態探索を用いてもよい。図27は、操作と状態遷移の例を示す。図26のシナリオを実行した結果を木構造で示している。例えば、5注文2によって状態22754まで進んだ後、初期状態2750までバックトラックが行われる。そして6注文2の操作が行われる。この場合、状態2においては、表2714に示されるように注文Noは、2まで増加しているが、状態3においては、表2716に示されるように、注文Noは、1となっており、本実施形態により、シーケンス番号のバックトラックが適切に行われていることが分かる。図28は、シーケンスバックトラック不能による不具合の例を示す。これは、例えば、図9におけるDBシーケンスバックトラック制御装置900を用いずに、DB接続切換部941を用いて、検査対象アプリケーションプログラム930を直接DBMS940に接続した場合の例を示している。図28の各々の注文Noは、DMBS940のシーケンス番号取得要求を用いているために、シーケンス番号のバックトラックが正常に行われていない。したがって、注文Noが、バックトラックできずに増加してしまっていることが分かる。シーケンスのバックトラックが出来ないと、注文処理ごとに注文Noシーケンスが増えてしまう。このため、以下のような不具合が発生する。1現状の注文Noの値によって注文数を算出するロジックがあった場合、注文数が間違ってしまう。2成功すべき検索が失敗してしまい、探索すべき状態に到達できない。3本来同じであるべき状態が、別の状態となってしまう。図29は、一実施形態のハードウエア構成を示している。ハードウエアには、CPU2902、メモリ2904、動的メモリ2906、媒体2909を読み書きするドライブ2908、通信インターフェース2910、表示装置2913等に画像信号を送るビデオインターフェース2912、I/Oインターフェース2914、I/Oとしてのキーボード2916、マウス2918、プリンタ2920が含まれる。CPU2902は、メモリ2904や動的メモリ2906に格納されている上記説明したプログラムモデル検査のための種々のプログラムを実行する。また、プログラムに係る本発明は、機械読み取り可能な記録媒体に格納されてもよい。機械読み取り可能な記録媒体には、磁気記録媒体、光ディスク、光磁気記録媒体、半導体メモリなどがある。磁気記録媒体には、HDD、フレキシブルディスクFD、磁気テープMTなどがある。光ディスクには、DVDDigitalVersatileDisc、DVD-RAM、CD-ROMCompactDisc-ReadOnlyMemory、CD-RRecordable/RWReWritableなどがある。また、光磁気記録媒体には、MOMagneto-Opticaldiskなどがある。以上の複数の実施形態に関し、更に以下の付記を開示する。付記1プログラムモデル検査装置用のDBシーケンスバックトラック制御プログラムであって、アプリケーションプログラムからのDB操作コマンドのシーケンス番号取得要求に応答して、DBMSに代わってシーケンス番号を出力することによって前記シーケンス番号取得要求の存在しないDB操作コマンドを前記DBMSに伝達すると共に前記シーケンス番号の状態の履歴を前記アプリケーションプログラムの状態と対応付けて記憶部に記憶し、前記プログラムモデル検査装置により指定されたアプリケーションプログラムの状態まで戻すバックトラック要求に応答して、前記記憶部に記憶された前記シーケンス番号の状態の履歴に基づいて、前記シーケンス番号の状態を、前記指定されたアプリケーションプログラムの状態と対応する状態までバックトラックさせる、処理をコンピュータに実行させることを特徴とするプログラム。付記2前記記憶部に記憶する処理は、アプリケーションプログラムからのDB操作コマンドを、シーケンス番号取得要求に係るDB操作コマンドと、その他のDB操作コマンドとに分離し、前記シーケンス番号取得要求に係るDB操作コマンドから、シーケンス番号取得要求を抽出し、前記抽出されたシーケンス番号取得要求に応答して、DBMSに代わって前記シーケンス番号を出力することによりシーケンス番号の状態の履歴をアプリケーションプログラムの状態と対応付けて記憶部に保存し、前記シーケンス番号取得要求に係るDB操作コマンドのうち、シーケンス番号取得要求が組み込まれたDB操作コマンドの中の前記組み込まれたシーケンス番号取得要求を、前記出力されたシーケンス番号に置換したDB操作コマンドと、前記その他のDB操作コマンドと、を前記DBMSに伝達する、処理を有することを特徴とする付記2記載のプログラム。付記3プログラムモデル検査装置用のDBシーケンスバックトラック制御方法であって、アプリケーションプログラムからのDB操作コマンドのシーケンス番号取得要求に応答して、DBMSに代わってシーケンス番号を出力することによって前記シーケンス番号取得要求の存在しないDB操作コマンドを前記DBMSに伝達すると共に前記シーケンス番号の状態の履歴を前記アプリケーションプログラムの状態と対応付けて記憶部に記憶し、前記プログラムモデル検査装置により指定されたアプリケーションプログラムの状態まで戻すバックトラック要求に応答して、前記記憶部に記憶された前記シーケンス番号の状態の履歴に基づいて、前記シーケンス番号の状態を、前記指定されたアプリケーションプログラムの状態と対応する状態までバックトラックさせる、ことを特徴とする方法。付記4前記記憶部に記憶する処理は、アプリケーションプログラムからのDB操作コマンドを、シーケンス番号取得要求に係るDB操作コマンドと、その他のDB操作コマンドとに分離し、前記シーケンス番号取得要求に係るDB操作コマンドから、シーケンス番号取得要求を抽出し、前記抽出されたシーケンス番号取得要求に応答して、DBMSに代わって前記シーケンス番号を出力することによりシーケンス番号の状態の履歴をアプリケーションプログラムの状態と対応付けて記憶部に保存し、前記シーケンス番号取得要求に係るDB操作コマンドのうち、シーケンス番号取得要求が組み込まれたDB操作コマンドの中の前記組み込まれたシーケンス番号取得要求を、前記出力されたシーケンス番号に置換したDB操作コマンドと、前記その他のDB操作コマンドと、を前記DBMSに伝達する、処理を有することを特徴とする付記3記載の方法。付記5プログラムモデル検査装置用のDBシーケンスバックトラック制御装置であって、アプリケーションプログラムからのDB操作コマンドのシーケンス番号取得要求に応答して、DBMSに代わってシーケンス番号を出力することによって前記シーケンス番号取得要求の存在しないDB操作コマンドを前記DBMSに伝達すると共に前記シーケンス番号の状態の履歴を前記アプリケーションプログラムの状態と対応付けて記憶部に記憶する、シーケンス番号処理部と、前記プログラムモデル検査装置により指定されたアプリケーションプログラムの状態まで戻すバックトラック要求に応答して、前記記憶部に記憶された前記シーケンス番号の状態の履歴に基づいて、前記シーケンス番号の状態を、前記指定されたアプリケーションプログラムの状態と対応する状態までバックトラックさせる、シーケンスバックトラック部と、を有することを特徴とする装置。付記6前記シーケンス番号処理部は、アプリケーションプログラムからのDB操作コマンドを、シーケンス番号取得要求に係るDB操作コマンドと、その他のDB操作コマンドとに分離し、前記シーケンス番号取得要求に係るDB操作コマンドから、シーケンス番号取得要求を抽出する、DB操作コマンド解析分離部と、前記抽出されたシーケンス番号取得要求に応答して、DBMSに代わって前記シーケンス番号を出力することによりシーケンス番号の状態の履歴をアプリケーションプログラムの状態と対応付けて記憶部に保存する、シーケンス管理部と、前記シーケンス番号取得要求に係るDB操作コマンドのうち、シーケンス番号取得要求が組み込まれたDB操作コマンドの中の前記組み込まれたシーケンス番号取得要求を、前記出力されたシーケンス番号に置換したDB操作コマンドと、前記その他のDB操作コマンドと、を前記DBMSに伝達する、DB操作コマンド置換部と、を有することを特徴とする付記5記載の装置。"