"修正対象アサーションを前記修正対象アサーションの論理構造に基づいて分解し、対象回路のシミュレーションを実行することにより、前記修正対象アサーションから分解されたプロパティ群の中から不成立になったプロパティを検出し、検出された不成立になったプロパティに、不成立の原因要素を論理和で結合し、結合されたプロパティを出力する、処理をコンピュータに実行させることを特徴とする修正プログラム。前記プロパティ群の木構造データを生成する処理を前記コンピュータに実行させ、前記検出する処理では、前記生成する処理によって生成された木構造データを構成するプロパティ群のうち最下層のプロパティから検出することを特徴とする請求項1に記載の修正プログラム。前記対象回路のシミュレーションを実行することによりアサーションごとの不成立回数を取得し、取得された不成立回数に基づいてアサーション群の中から前記修正対象アサーションを選択する、処理を前記コンピュータに実行させ、前記分解する処理では、前記選択する処理によって選択された修正対象アサーションを前記アサーションの論理構造に基づいて分解することを特徴とする請求項1または2に記載の修正プログラム。修正対象アサーションごとに、前記結合する処理によって結合する都度、結合されたプロパティについての結合前の不成立回数を累積し、前記修正対象アサーションごとに、累積された不成立回数が、修正対象アサーションの不成立回数に到達したか否かを判断する、処理を前記コンピュータに実行させ、前記検出する処理では、前記判断する処理によって到達したと判断された修正対象アサーションの木構造データから検出しないことを特徴とする請求項3に記載の修正プログラム。修正対象アサーションを前記修正対象アサーションの論理構造に基づいて分解する分解手段と、対象回路のシミュレーションを実行することにより、前記分解手段によって前記修正対象アサーションから分解されたプロパティ群の中から不成立になったプロパティを検出する検出手段と、前記検出手段によって検出された不成立になったプロパティに、不成立の原因要素を論理和で結合する結合手段と、前記結合手段によって結合されたプロパティを出力する出力手段と、を備えることを特徴とする修正装置。修正対象アサーションを前記修正対象アサーションの論理構造に基づいて分解し、対象回路のシミュレーションを実行することにより、前記修正対象アサーションから分解されたプロパティ群の中から不成立になったプロパティを検出し、検出された不成立になったプロパティに、不成立の原因要素を論理和で結合し、結合されたプロパティを出力する、処理をコンピュータが実行することを特徴とする修正方法。アサーションの作成元となる仕様書について、検証者が理解不足であったり誤解している場合、作成されたアサーションに誤りが存在する。このようなアサーションを用いて対象回路のシミュレーションを実行して、アサーションが不成立になった場合、アサーションが正しくて不成立になったかアサーションに誤りがあったために不成立になったかの判別がつかない。また、不成立の原因となるシミュレーション結果は、アサーションの内容により複数とおり出現することもある。したがって、検証者が自ら仕様書を再分析して、または検証者が設計者とともに仕様書を再確認し、その上でアサーションを修正する必要がある。これにより、アサーションの修正作業に時間がかかる。また、上述した従来技術では、アサーション自体が正しいものであるとの前提で処理をおこなっているため、仕様書の理解不足や誤解に基づくアサーションの誤りを特定することは困難である。本発明の一側面では、アサーションの修正作業の効率化を図ることができる修正プログラム、修正装置、および修正方法を提供することを目的とする。本発明の一側面として、修正対象アサーションを前記修正対象アサーションの論理構造に基づいて分解し、対象回路のシミュレーションを実行することにより、前記修正対象アサーションから分解されたプロパティ群の中から不成立になったプロパティを検出し、検出された不成立になったプロパティに、不成立の原因要素を論理和で結合し、結合されたプロパティを出力する修正プログラム、修正装置、および修正方法が提案される。本発明の一側面によれば、アサーションの修正作業の効率化を図ることができるという効果を奏する。以下に添付図面を参照して、この発明にかかる修正プログラム、修正装置、および修正方法の実施の形態を詳細に説明する。本実施の形態では、対象回路のシミュレーションにより不成立失敗となったアサーションを修正対象とする。ここで、アサーションとは、対象回路の設計が満たすべき性質を記述した情報である。SVASystemVerilogAssertionを例に挙げると、プロパティとしてA==Bが記述されている場合、変数/信号Aが常に変数/信号Bと同じであることを確認すべきことを意味している。また、プロパティとしてA|->Bが記述されている場合、イベントAが発生した場合、イベントBが発生することを確認すべきことを意味している。また、プロパティとしてABが記述されている場合、ビット値Aおよびビット値Bが常に1に設定されることを確認すべきことを意味している。アサーションが成立していれば、対象回路は仕様書どおりに振舞っていることがわかる。一方、アサーションが不成立であれば、対象回路は仕様書どおりに動作していないことがわかる。ここで、検証者が対象回路の仕様書について理解不足であったり、誤解をしていた場合、アサーションが不成立になっても、仕様書にはない動作による不成立であるか仕様書どおりの動作であるにもかかわらずアサーションの誤りによる不成立であるかの判別がつかない。そこで、本実施の形態では、不成立のあったアサーションについて、不成立の原因となった要素変数、信号、ビット値を不成立のあったアサーションに対し論理和で追加する。また、アサーション自体は、複雑な記述や冗長な記述となっている場合が多い。したがって、不成立となったアサーションのどの箇所を修正すべきか検証者が確認する必要がある。したがって、本実施の形態では、シミュレーションに先立って、アサーションを分解する。本実施の形態では、分解された記述をプロパティと称す。プロパティは、上述したA==B、A|->B、ABのような単純な式である。したがって、シミュレーションにおいて不成立となったプロパティに対し修正したり修正案を提示することで、修正作業の効率化を図る。<アサーション修正例>図1は、本実施の形態にかかるアサーション修正例を示す説明図である。図1において、アサーションA5は、対象回路DUTの設計情報101によるシミュレーションで不成立となったアサーションである。アサーションA5は、複数のプロパティp1~p4が論理和||または論理積で結合された情報である。したがって、修正装置100は、アサーションA5を論理和および論理積の箇所を境界にして分解する。図1では、アサーションA5は、プロパティp1~p4に分解される。分解されたプロパティp1~p4は、アサーションA5の論理構造にしたがって木構造データT5となる。プロパティp1~p4は、テストベンチ102に組み込まれ図1では例としてp1、対象回路DUTの設計情報101を用いた対象回路DUTのシミュレーションにより、成立、不成立が判断される。たとえば、クロックの立ち上がり時に、レジスタRb,Rcのビット値B,Cが0、レジスタRxのビット値Xが1になった場合、プロパティp1は不成立となる。この場合、修正装置100は、プロパティp1に、||Xを追加することで、プロパティp1を修正する。したがって、修正後にシミュレーションを実行すると、クロックの立ち上がり時に、レジスタRb,Rcのビット値B,Cが0、レジスタRxのビット値Xが1になった場合、修正プロパティP1は成立することになる。<修正対象の絞込み例>図2は、修正対象の絞込み例を示す説明図である。図2では、図1のアサーションの分解に先立って、修正対象のアサーションを絞り込む。これにより、誤りが潜んでいる可能性が高いアサーションを優先的に抽出することができる。具体的には、アサーション群が組み込まれたテストベンチ102と対象回路DUTの設計情報101とを用いた対象回路DUTのシミュレーションにより、修正装置100は、シミュレーション結果200を得る。シミュレーション結果200では、アサーションごとにアサーションIDと不成立回数が記憶されている。アサーションIDは、アサーションを特定する識別コードである。本例では、説明の都合上、アサーションに割り当てた符号を識別コードとしている。不成立回数とは、シミュレーション時にアサーションが成立しなかった回数であり、シミュレーション中に計数される。この不成立回数には、不成立の原因が複数とおりある場合、それらの不成立回数が混在する。たとえば、アサーションA5の不成立回数は20であるが、プロパティp1~p4での不成立回数の合計が20回であることを意味しており、内訳はプロパティごとに異なる。たとえば、プロパティp1が13回、プロパティp2が7回、プロパティp3,p4が0回である場合、プロパティp3,p4については修正する必要がないことがわかる。このように、アサーションを分解することで、修正すべきプロパティと修正すべきでないプロパティを特定することができる。図3は、シミュレーション結果200の選択画面例を示す説明図である。図3では、シミュレーション結果200が選択画面300に表示されている。具体的には、たとえば、アサーションごとに、アサーションIDと不成立回数とチェックボックスとが表示されている。不成立回数が多いアサーションほど誤りが潜んでいる可能性が高い。したがって、検証者は、マウスなどの入力装置を操作して、修正したいアサーションのチェックボックス301にチェックを入れて、確認ボタン302を押下することで、修正対象アサーションが決定される。図3の場合、アサーションA5,A7,A4,A2が修正対象アサーションとなる。なお、図2および図3では、不成立回数を記憶、表示させているが、不成立確率=不成立回数/成立回数不成立回数を記憶、表示させることとしてもよい。図4は、木構造データを示す説明図である。木構造データは、図1に示したように、アサーションをその論理構造で分解し、関連しあうプロパティを連結した構造体である。図4において、○は木構造データの節点であり、プロパティを示す。○内の符号でプロパティを示している。木構造データは修正対象アサーションごとに生成される。各木構造データの最上位階層を第1階層とし、階層が下がるごとに階層番号rが増加する。図4の場合は、アサーションA7の第5階層が最下位階層となる。図5は、修正対象アサーションから分解されたプロパティ群での対象回路DUTの再シミュレーション結果500を示す説明図である。図5では、プロパティごとに、プロパティID、不成立回数、および不成立原因要素が記憶される。プロパティIDは、プロパティを特定する識別コードである。本例では、説明の都合上、プロパティに割り当てた符号を識別コードとしている。不成立回数とは、シミュレーション時にプロパティが成立しなかった回数であり、再シミュレーション中に計数される。不成立原因要素とは、プロパティが不成立となった原因を示す要素である。たとえば、プロパティp1の不成立原因要素はXとなっている。すなわち、レジスタRb,Rcのビット値BまたはCの少なくともいずれか一方が1になるべきところ、いずれも0で、レジスタRXのビット値XがX=1になったために、不成立になったことを示している。また、プロパティp2の不成立原因要素はE==3となっている。すなわち、プロパティp2ではD=1の1サイクル後にE==2となるべきところ、E==3になったために、不成立になったことを示している。また、プロパティp5の不成立原因要素はG==Jとなっている。すなわち、プロパティp5では、変数/信号Gが常に変数/信号Hと同じであるべきところ、G==Jになったために、不成立になったことを示している。<プロパティ修正例>図6~図8は、プロパティ修正例を示す説明図である。図6は、プロパティp2の修正例を示している。プロパティp2では、D=1の1サイクル後にE==2となるべきところ、E==3になったために、不成立になっている。したがって、修正装置100は、プロパティp2に不成立原因要素であるE==3を論理和で結合する。これにより、プロパティp2が修正プロパティP2となる。したがって、次回のシミュレーションで、D==1の1サイクル後は、E==2またはE==3のいずれかになれば、修正プロパティP2が成立することになる。図7は、プロパティp1の修正例を示している。プロパティp1では、レジスタRb,Rcのビット値BまたはCの少なくともいずれか一方が1になるべきところ、いずれも0で、レジスタRXのビット値xがX=1になったために、不成立になっている。したがって、修正装置100は、プロパティp1に不成立原因要素であるXを論理和で結合する。これにより、プロパティp1が修正プロパティP1となる。したがって、次回のシミュレーションで、レジスタRb,Rc,Rxのビット値B,CまたはXの少なくともいずれか一つが1になれば、修正プロパティP1が成立することになる。図8は、プロパティp5の修正例を示している。プロパティp5では、変数/信号Gが常に変数/信号Hと同じであるべきところ、G==Jになったために、不成立になっている。したがって、修正装置100は、プロパティp5に不成立原因要素であるG==Jを論理和で結合する。これにより、プロパティp5が修正プロパティP5となる。したがって、次回のシミュレーションで、G==HまたはG==Jのいずれかになれば、修正プロパティP5が成立することになる。<修正装置100のハードウェア構成例>図9は、実施の形態にかかる修正装置100のハードウェア構成例を示すブロック図である。図9において、修正装置100は、CPUCentralProcessingUnit901と、ROMRead‐OnlyMemory902と、RAMRandomAccessMemory903と、磁気ディスクドライブ904と、磁気ディスク905と、光ディスクドライブ906と、光ディスク907と、ディスプレイ908と、I/FInterface909と、キーボード910と、マウス911と、スキャナ912と、プリンタ913と、を備えている。また、各構成部はバス900によってそれぞれ接続されている。ここで、CPU901は、修正装置100の全体の制御を司る。ROM902は、ブートプログラムなどのプログラムを記憶している。RAM903は、CPU901のワークエリアとして使用される。磁気ディスクドライブ904は、CPU901の制御にしたがって磁気ディスク905に対するデータのリード/ライトを制御する。磁気ディスク905は、磁気ディスクドライブ904の制御で書き込まれたデータを記憶する。光ディスクドライブ906は、CPU901の制御にしたがって光ディスク907に対するデータのリード/ライトを制御する。光ディスク907は、光ディスクドライブ906の制御で書き込まれたデータを記憶したり、光ディスク907に記憶されたデータをコンピュータに読み取らせたりする。ディスプレイ908は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイ908は、たとえば、CRT、TFT液晶ディスプレイ、プラズマディスプレイなどを採用することができる。インターフェース以下、I/Fと略する。909は、通信回線を通じてLANLocalAreaNetwork、WANWideAreaNetwork、インターネットなどのネットワーク914に接続され、このネットワーク914を介して他の装置に接続される。そして、I/F909は、ネットワーク914と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。I/F909には、たとえばモデムやLANアダプタなどを採用することができる。キーボード910は、文字、数字、各種指示などの入力のためのキーを備え、データの入力をおこなう。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウス911は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などをおこなう。ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。スキャナ912は、画像を光学的に読み取り、修正装置100内に画像データを取り込む。なお、スキャナ912は、OCROpticalCharacterReader機能を持たせてもよい。また、プリンタ913は、画像データや文書データを印刷する。プリンタ913には、たとえば、レーザプリンタやインクジェットプリンタを採用することができる。<修正装置100の機能的構成例>図10は、修正装置100の機能的構成を示すブロック図である。修正装置100は、実行部1001と、取得部1002と、選択部1003と、分解部1004と、生成部1005と、検出部1006と、結合部1007と、算出部1008と、判断部1009と、出力部1010と、を備えている。実行部1001~出力部1010は、は、具体的には、たとえば、図9に示したROM902、RAM903、磁気ディスク905、光ディスク907などの記憶装置に記憶されたプログラムをCPU901に実行させることにより、または、I/F909により、その機能を実現する。実行部1001は、対象回路DUTの設計情報101によるシミュレーションを実行する。具体的には、たとえば、図2に示したように、実行部1001は、シミュレーションを実行する。また、実行部1001は、シミュレーション中に、アサーションが成立成功するか不成立になる失敗かを判断する。不成立の場合は、アサーションごとに不成立回数を計数して、図2に示したようにシミュレーション結果200として記憶装置に記憶する。取得部1002は、対象回路DUTのシミュレーションを実行することによりアサーションごとの不成立回数を取得する。具体的には、たとえば、図2に示したシミュレーション結果200が実行部1001により記憶装置に記憶されるため、取得部1002は、記憶装置のシミュレーション結果200の中からアサーションごとの不成立回数を読み出す。選択部1003は、取得部1002によって取得された不成立回数に基づいてアサーション群の中から修正対象アサーションを選択する。具体的には、たとえば、取得部1002によって取得された不成立回数に基づいて図3に示した選択画面300が表示される。したがって、検証者は、マウス911などの入力装置を操作して修正したいアサーションのチェックボックス301にチェックを入れ、確認ボタン302を押下する。これにより、選択部1003は、チェックボックス301にチェックが入れられたアサーションを修正対象アサーションであると認識する。分解部1004は、修正対象アサーションをアサーションの論理構造に基づいて分解する。分解対象となる修正対象アサーションは、検証者が任意に決めてもよく、また、選択部1003によって選択されたアサーションを修正対象アサーションとしてもよい。分解部1004では、図1に示したように、論理和または論理積で結合されている式をプロパティとして抽出する。抽出されたプロパティ群は修正対象アサーションごとに記憶装置に記憶される。生成部1005は、分解部1004によって分解されたプロパティ群の木構造データを生成する。具体的には、たとえば、生成部1005は、修正対象アサーションごとに得られたプロパティ群内の包含関係により木構造データを生成する。たとえば、プロパティp4にはプロパティp2,p3が包含されているため、プロパティp2,p3は、プロパティp4の下位階層のプロパティとして連結される。プロパティp3にはプロパティp1が包含されているため、プロパティp1は、プロパティp3の下位階層のプロパティとして連結される。これにより、図4に示したような木構造データが修正対象プロパティごとに生成されることになる。また、実行部1001は、図1に示したように、分解されたプロパティ群を用いて対象回路DUTのシミュレーション再シミュレーションを実行する。再シミュレーションでは、プロパティごとに不成立回数を計数し、不成立原因要素を検出する。これにより、図5に示したような再シミュレーション結果500が得られる。再シミュレーション結果500は、記憶装置に記憶される。検出部1006は、対象回路DUTのシミュレーションを実行することにより、分解部1004によって修正対象アサーションから分解されたプロパティ群の中から不成立になったプロパティを検出する。具体的には、たとえば、検出部1006は、再シミュレーション結果500の中で所定回数たとえば1回以上不成立となったプロパティを修正対象プロパティとして検出する。また、検出部1006は、生成部1005によって生成された木構造データを構成するプロパティ群のうち最下層のプロパティから検出する。たとえば、図4の例では、第5階層のプロパティp5,p6を検出し、つぎに、第4階層のプロパティp7,p11を検出し、つぎに、第3階層のプロパティp1、p8、p12~p14を検出する。このように、段階的に階層を上げていき、検出部1006は、最終的に第1階層のプロパティp4、p10、p17,18を検出することになる。また、検出部1006は、再シミュレーション結果500から修正対象プロパティの不成立原因要素を検出する。結合部1007は、検出部1006によって検出された不成立になったプロパティに、不成立の原因要素を論理和で結合する。結合部1007は、具体的には、たとえば、図6~図8に示したように、論理和で結合する。算出部1008は、修正対象アサーションごとに、結合部1007によって結合する都度、結合されたプロパティについての結合前の不成立回数を累積する。たとえば、修正対象アサーションA5のプロパティp1~p4を例に挙げると、修正対象アサーションA5の不成立回数は20回図2を参照であり、プロパティp1の不成立回数は13回、プロパティp2の不成立回数は7回、プロパティp3,p4の不成立回数はともに0回である図5を参照。まず、累積不成立回数の初期値は0である。検出部1006は、最下層である第5階層から順次修正対象プロパティを検出するため、修正対象アサーションA5の木構造データT5については、第3階層のプロパティp1が最初に検出されて、結合部1007により結合が行われる。このとき、プロパティp1の不成立回数は13回であるため、累積不成立回数に累積することで、013=13回となる。つぎに、第2階層のプロパティp2が検出されて、結合部1007により結合が行われる。このとき、プロパティp2の不成立回数は7回であるため、累積不成立回数に累積することで、137=20回となる。判断部1009は、修正対象アサーションごとに、算出部1008によって累積された不成立回数が、修正対象アサーションの不成立回数に到達したか否かを判断する。具体的には、累積される都度、判断部1009は、修正対象アサーションの不成立回数に到達したか否かを判断する。たとえば、上記の例で、第2階層のプロパティp2が検出されて、累積不成立回数が、137=20回となった場合、修正対象アサーションA5の不成立回数20回に到達したと判断する。この場合、検出部1006は、木構造データT5については、これ以上、不成立のプロパティp3,p4の検出はおこなわない。すなわち、検出処理を実行しても、不成立のプロパティは得られないため、木構造データT5を検出対象から除外する。たとえば、検出不可フラグを設定したり、木構造データT5を消去したりする。これにより、修正処理の高速化を図ることができる。出力部1010は、結合部1007によって結合されたプロパティを出力する。具体的には、たとえば、出力部1010は、結合されたプロパティ、すなわち、修正済みのプロパティを出力する。また、修正する必要がなかったプロパティも出力する。これらのプロパティをまとめて修正プロパティ群と称す。修正プロパティ群は、ディスプレイ908に出力することで、表示される。また、プリンタ913に出力されることで印刷される。また、I/F909に出力されることで、外部装置に送信される。また、記憶装置に出力されることで、修正プロパティ群が保存される。<修正処理手順>図11は、修正装置100による修正処理手順を示すフローチャートである。まず、修正装置100は、図2に示したようなシミュレーション結果200を取得してステップS1101、不成立回数の降順にアサーションを並び替えるステップS1102。そして、修正装置100は、図3に示したような、並び替え後のアサーションを示す選択画面300をディスプレイ908に表示するステップS1103。修正装置100は、選択部1003により選択入力があった場合ステップS1104:Yes、選択アサーションIDを保持してステップS1105、ステップS1106に移行する。一方、選択入力がない場合ステップS1104:No、ステップS1106に移行する。ステップS1106において、修正装置100は、選択画面300の確認ボタン302の選択入力による確定選択があったか否かを判断するステップS1106。確定選択がない場合ステップS1106:No、ステップS1104に戻る。一方、確定選択があった場合ステップS1106:Yes、修正装置100は、選択アサーションIDがあるか否かを判断するステップS1107。選択アサーションIDがない場合ステップS1107:No、アサーションを1つも選択せずに確定選択をしたこととなり、一連の処理を終了する。一方、選択アサーションIDがある場合ステップS1107:Yes、選択アサーションIDを手がかりにして、シミュレーション結果200から選択アサーションを抽出するステップS1108。そして、抽出された選択アサーションは修正対象アサーションになるため、修正装置100は、修正対象アサーションについて修正処理を実行するステップS1109。修正処理ステップS1109の詳細は図12で後述する。修正処理ステップS1109後、修正装置100は、出力部1010により、修正プロパティ群を出力するステップS1110ことで、一連の処理を終了する。なお、修正プロパティ群については、検証者がマウス911やキーボード910などの入力装置を操作することで、適宜修正をおこなってもよい。図12は、図11に示した修正処理ステップS1109の詳細な処理手順例を示すフローチャートである。まず、修正装置100は、未選択の修正対象アサーションがあるか否かを判断するステップS1201。未選択の修正対象アサーションがある場合ステップS1201:Yes、修正装置100は、選択部1003により未選択の修正対象アサーションを選択しステップS1202、分解部1004により、修正対象アサーションを分解するステップS1203。そして、修正装置100は、生成部1005により、分解されたプロパティ群で修正対象アサーションの木構造データを生成してステップS1204、ステップS1201に戻る。また、ステップS1201において、未選択の修正対象アサーションがない場合ステップS1201:No、修正装置100は、階層番号rをr=Rに設定するステップS1205。Rは、生成された木構造データ群の最下層である。図4の例ではR=5となる。つぎに、修正装置100は、実行部1001により、プロパティ群木構造データ群を用いて対象回路DUTの再シミュレーションを実行するステップS1206。そして、修正装置100は、検出部1006により、木構造データ群の第r階層のプロパティから不成立のプロパティを検出するステップS1207。つぎに、修正装置100は、図6~図8に示したように、結合部1007により、不成立のプロパティの不成立原因要素を、論理和で不成立のプロパティに結合するステップS1208。そして、修正装置100は、算出部1008により修正済みプロパティの不成立回数を修正対象アサーションごとに累積計算するステップS1209。このあと、修正装置100は、判断部1009により、修正対象アサーションごとに、修正対象アサーションの不成立回数に到達したか否かを判断するステップS1210。到達していない修正対象アサーションについてはステップS1210:No、ステップS1212に移行する。一方、到達した修正対象アサーションについてはステップS1210:Yes、到達した修正対象アサーションの木構造データを修正対象外に設定しステップS1211、ステップS1212に移行する。これにより、以降の修正処理の高速化を図ることができる。ステップS1212では、修正装置100は、階層番号rをデクリメントしステップS1212、r=0であるか否かを判断するステップS1213。r=0でない場合ステップS1213:No、ステップS1207に戻る。一方、r=0である場合ステップS1213:Yes、修正処理ステップS1109を終了し、ステップS1110に移行する。なお、上述した修正処理ステップS1109においては、ステップS1209~S1211を省略してもよい。このように、本実施の形態によれば、不成立となったアサーションをプロパティ群に分解し、不成立のプロパティごとに、不成立原因要素を論理和で結合するため、修正処理の自動化を図ることができる。また、アサーションではなくプロパティ単位で修正処理をおこなうため、修正箇所を人手で探さずに自動で修正箇所を突き止めることができる。したがって、修正処理の高速化を図ることができる。また、木構造データの最下層から不成立のプロパティを検出していくことで、不成立の根本原因となるプロパティを早期に突き止めることができる。また、修正対象アサーションの不成立回数に到達した場合は、その修正対象の木構造データからはこれ以上、不成立のプロパティが存在しないため、そのような木構造データについては検出処理の実行をスキップすることで、修正処理の高速化を図ることができる。以上のことから、本実施の形態によれば、理解不足や誤解がある状態でアサーションが作成された場合であっても、修正すべきプロパティを自動的に突き止めることができ、そのようなプロパティに対し適切な修正処理を自動実行することができる。したがって、検証者が自ら仕様書を再分析して、または検証者が設計者とともに仕様書を再確認し、その上でアサーションを修正するといった作業負担が軽減し、アサーションの修正作業時間の短縮化を図ることができる。また、これにより、アサーションの修正作業の効率化を図ることができる。なお、本実施の形態で説明した修正方法は、予め用意されたプログラムをパーソナルコンピュータやワークステーション等のコンピュータで実行することにより実現することができる。本修正プログラムは、ハードディスク、フレキシブルディスク、CD-ROM、MO、DVD等のコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。また本修正プログラムは、インターネット等のネットワークを介して配布してもよい。"