(57)【要約】【課題】  可変長データ構造を扱うソフトウェアのプロパティ整合性判定処理にＳＭＴソルバを適用できるようにする。【解決手段】  述語毎最短レコード長抽出器２は，ソフトウェアのプロパティから，述語一覧記憶部１２に該当する述語を抽出して，述語を満たすレコード長の最短レコード長を特定する。判定述語抽出器３は，抽出された述語からその述語が処理するレコードセットと判定条件を定める判定述語とを抽出して，レコードセットごとに抽出した判定述語をまとめて判定述語集合を生成する。レコード長決定器４は，各判定述語集合の充足可能性を判定して，その判定処理の結果にもとづいて，判定述語集合に対応するレコードセットのレコード長を算出する。【選択図】  図１
2011013797.tif 000002
【特許請求の範囲】
【請求項１】
コンピュータを、
検査対象のソフトウェアの論理的仕様を、処理対象のレコードセットの識別子と判定条件に関する判定述語により定義した述語を記憶するプロパティ記憶手段と，
前記プロパティ記憶手段から，レコード長に関する制約を有する述語を抽出して述語一覧記憶部に記憶する手段と，
前記述語一覧記憶部に記憶された各述語について、充足可能性判定に必要な最短レコード長を特定する述語毎最短レコード長抽出手段と，
前記プロパティ記憶手段に記憶された前記述語に含まれる前記判定述語を、前記レコードセットの識別子ごとにまとめた判定述語集合を生成する判定述語抽出手段と，
前記判定述語抽出手段で生成された前記判定述語集合に基づいて生成した論理式により、該判定述語集合の充足可能性を判定する判定手段と，
前記判定手段において，判定述語集合が充足可能であると判定された場合に，当該判定述語集合を構成する各判定述語に対応する各述語の前記最短レコード長を抽出し，抽出した各最短レコード長のうちの最長値を，当該判定述語集合に対応するレコードセットの識別子で特定されるレコードセットのレコード長に設定するレコード長決定手段
として機能させるレコード長決定プログラム。
【請求項２】
前記判定手段において，判定述語集合が充足不能であると判定された場合に，
前記レコード長決定手段は，当該判定述語集合を構成する各判定述語に対応する各述語の前記最短レコード長を抽出して，抽出した各最短レコード長の総和を，当該判定述語集合に対応するレコードセットの識別子で特定されるレコードセットのレコード長に設定する
ことを特徴とする請求項１に記載のレコード長決定プログラム。
【請求項３】
前記判定手段において，前記判定述語集合が充足不能であると判定された場合に，
前記レコード長決定手段は，当該判定述語集合のべき集合を生成して，前記生成したべき集合に含まれる部分集合のうち空集合を除くもの各々の充足可能性を判定する処理と，
前記判定述語集合を構成する前記部分集合の組み合わせを生成する処理と，
前記部分集合の充足可能性の判定結果をもとに，前記生成した部分集合の組み合わせから，組み合わせを構成する部分集合が全て充足可能である組み合わせを抽出する処理と，
前記抽出された組み合わせについて，当該組み合わせを構成する部分集合各々について，当該部分集合を構成する判定述語に対応する述語の最短レコード長を抽出して，前記抽出した最短レコード長の最長値を求め，前記求めた最長値の総和を前記組み合わせの必要レコード長とする処理と，
前記組み合わせの必要レコード長のうち最短値を、当該判定述語集合に対応するレコードセットの識別子で特定されるレコードセットのレコード長に設定する処理とを行う
ことを特徴とする請求項１記載のレコード長決定プログラム。
【請求項４】
前記レコード長決定手段は，
前記生成した組み合わせから，組み合わせを構成する部分集合が全て充足可能である組み合わせが抽出されなかった場合に，前記生成した組み合わせ各々について，前記充足可能な部分集合を構成する判定述語に対応する述語の最短レコード長のうちの最長値を求める処理と，
前記充足不能な部分集合を構成する判定述語に対応する述語の最短レコード長の総和を求める処理と，
前記求めた最長値と総和との合計を前記組み合わせの必要レコード長とする処理とを行う
ことを特徴とする請求項３に記載のレコード長決定プログラム。
【請求項５】
検査対象のソフトウェアの論理的仕様を、処理対象のレコードセットの識別子と判定条件に関する判定述語により定義した述語を記憶するプロパティ記憶手段と，
前記プロパティ記憶手段から，レコード長に関する制約を有する述語を抽出して述語一覧記憶部に記憶する手段と，
前記述語一覧記憶部に記憶された各述語について、充足可能性判定に必要な最短レコード長を特定する述語毎最短レコード長抽出手段と，
前記プロパティ記憶手段に記憶された前記述語に含まれる前記判定述語を、前記レコードセットの識別子ごとにまとめた判定述語集合を生成する判定述語抽出手段と，
前記判定述語抽出手段で生成された前記判定述語集合に基づいて生成した論理式により、該判定述語集合の充足可能性を判定する判定手段と，
前記判定手段において，判定述語集合が充足可能であると判定された場合に，当該判定述語集合を構成する各判定述語に対応する各述語の前記最短レコード長を抽出し，抽出した各最短レコード長のうちの最長値を，当該判定述語集合に対応するレコードセットの識別子で特定されるレコードセットのレコード長に設定するレコード長決定手段とを備える
ことを特徴とするレコード長決定装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は，ソフトウェア検証におけるレコード長決定プログラムまたはレコード長決定装置に関する。
【背景技術】
【０００２】
ソフトウェア検証では，検証対象となるソフトウェアを抽象化したモデルを用いて，ソフトウェアの形式が，確認したい性質（仕様）を満たすかどうかを論理的に検証するモデル検証が行われる。
【０００３】
このモデル検証の仕様は，論理式として記述しておく必要があり，この記述をプロパティと呼ぶ。プロパティは，各イベントに対して，“Ａ−＞Ｂ”（イベントが条件Ａで生じたら，結果Ｂとなる）という論理式記述のように，形式的に表現されなければならない。例えば，上記の“Ａ−＞Ｂ”で，Ａ，Ｂの各項は，以下の例のように，整数値型，組型，レコード型を扱う述語論理式をとることができる。
【０００４】
Ａ：＝（ｘ＞０）ａｎｄ（（ｓｅｌｅｃｔ  ｙ  １）＜＝０）
ここで，ｓｅｌｅｃｔ  ｙ  １は，１番目の要素（ｉｎｔ型）と読む
Ｂ：＝（ａ＝１）ａｎｄ（ｂ＝０）
しかし，プロパティを表現する論理式記述は，一般的に複雑になるため，検証前に用意したプロパティ自体に矛盾が含まれる可能性がある。
【０００５】
例えば，上記論式のＡが，
Ａ：＝（ｘ＞０）ａｎｄ（（（ｓｅｌｅｃｔ  Ｂ  １）＜＝１０）  ｏｒ  （（ｓｅｌｅｃｔ  Ｂ  ２）＜０））  ａｎｄ  （ｘ＜−１）
である場合に，「Ａ」は“真”にならず，“Ａ−＞Ｂ”が，プロパティの仕様として意味をなさないものになる。したがって，ソフトウェア検証前に，プロパティ自体の整合性を判定する必要がある。
【０００６】
ところで，論理式が矛盾していないことを示すためには，論理式全体を真とするような各部分論理式の真偽時の組み合わせが存在することを示せばよい。論理式の無矛盾性を調べる処理として，充足可能であるか（真に成り得るか）否かを判定する処理として充足可能性判定処理器（ＳＡＴソルバ）が適用される。
【０００７】
また，最近では，ＳＭＴ（Ｓａｔｉｓｆｉａｂｉｌｉｔｙ  Ｍｏｄｕｌｏ  Ｔｈｅｏｒｉｅｓ）ソルバと呼ばれる充足可能性判定処理器が知られている。一般的に，ＳＡＴソルバはブール変数のみを扱うが，ＳＭＴソルバは，整数，実数，配列等を扱うことができるという利点がある。
【０００８】
なお，ＳＡＴソルバにおいて，限量記号付きブール式（ＱＢＦ）の従属可能性を判定するために，ＱＢＦを分析可能な構成要素に分解し，分解した各構成要素について独立または並列に充足可能性を分析していくことにより，限量記号を外したブール式として扱う手法が知られている。
【先行技術文献】
【特許文献】
【０００９】
【特許文献１】特開２００６−２０２２８８号公報
【発明の概要】
【発明が解決しようとする課題】
【００１０】
業務アプリケーションのソフトウェア検証において，業務仕様を記述するためには，表形式，データベーステーブルなどの可変長データ構造や，可変長のデータを処理する関数が定義できることが不可欠である。
【００１１】
しかし，従来のＳＭＴソルバでは，充足可能性判定の範囲が有限であることを前提にしている。そのため，ＳＭＴソルバが処理可能な入力言語では，可変長のデータ構造のデータ，可変長データを処理する関数や述語（例えば再帰的または可変的な繰り返し構造を持つ関数）を定義することができなかった。
【００１２】
具体的には，業務アプリケーションのテーブルとして，ＩＤ，名前，年齢，所属等のデータ項目を持つ社員情報テーブル（社員情報Ｔ）についてのプロパティ（事前条件）として，
「社員情報テーブル内に，所属が“ｓｏｆｔｗａｒｅ”な社員情報が存在し，かつ，…」
がある場合に，この事前条件の論理式に，
Ａ：＝ｅｘｉｓｔ（社員情報Ｔ，社員情報．所属＝＝“ｓｏｆｔｗａｒｅ”）ａｎｄ…
があるとする。また，述語ｅｘｉｓｔが，レコードセットと判定述語を引数として，判定関数を満たすレコードがレコードセット内に存在する場合に“ｔｒｕｅ”を返却するものであるとする。
【００１３】
すると，以下のような，述語ｅｘｉｓｔによる一般的な再帰的定義は，ＳＭＴソルバで処理することができない。
【００１４】
ｆｕｎ  ｅｘｉｓｔ（［］，ｐｒｅｄ）＝ｆａｌｓｅ
｜ｅｘｉｓｔ（ｒ：：ｒｓ，ｐｒｅｄ）＝ｉｆ  ｐｒｅｄ（ｒ）  ｔｈｅｎ  ｔｒｕｅ
ｅｌｓｅ  ｅｘｉｓｔ（ｒｓ，ｐｒｅｄ）
本願の発明者が検討したところによれば，検証対象のソフトウェアのリスト，テーブルデータ等の可変長データ処理に関連する関数を，ＳＭＴソルバで処理可能にするために，予め，所定の固定長に対応した関数を個別に定義するというアプローチが考えられる。
【００１５】
しかし，最適なデータ長で固定化することは容易ではない。
【００１６】
固定化のために設定したデータ長が長すぎる場合に，探索空間が膨大化してＳＭＴソルバの処理性能に大きく影響を与えてしまう。一方，設定したデータ長が短すぎる場合に，探索空間が小さ過ぎて，本来であれば充足可能である対象の充足可能を検出できなくなり，正しい解を得ることができないという問題が生じる。
【００１７】
本願発明の目的は，ソフトウェアのプロパティ整合性判定処理にＳＭＴソルバを適用可能とするために，プロパティ内の可変長データセットのレコード長を固定化するための最適なデータ長を設定することが可能な処理手段として，コンピュータを機能させるプログラム，および前記処理手段を備える処理装置を提供することである。
【００１８】
なお，本発明の前記および他の目的ならびに新規な特徴は，明細書の記述および添付図面から明らかになるものである。
【課題を解決するための手段】
【００１９】
本願において開示されるレコード長決定プログラムまたはレコード長決定装置の代表的なものの概要を簡単に説明すれば，以下のとおりである。
【００２０】
すなわち，レコード長決定プログラムは，コンピュータを、検査対象のソフトウェアの論理的仕様を、処理対象のレコードセットの識別子と判定条件に関する判定述語により定義した述語を記憶するプロパティ記憶手段と，前記プロパティ記憶手段から，レコード長に関する制約を有する述語を抽出して述語一覧記憶部に記憶する手段と，前記述語一覧記憶部に記憶された各述語について、充足可能性判定に必要な最短レコード長を特定する述語毎最短レコード長抽出手段と，前記プロパティ記憶手段に記憶された前記述語に含まれる前記判定述語を、前記レコードセットの識別子ごとにまとめた判定述語集合を生成する判定述語抽出手段と，前記判定述語抽出手段で生成された前記判定述語集合に基づいて生成した論理式により、該判定述語集合の充足可能性を判定する判定手段と，前記判定手段において，判定述語集合が充足可能であると判定された場合に，当該判定述語集合を構成する各判定述語に対応する各述語の前記最短レコード長を抽出し，抽出した各最短レコード長のうちの最長値を，当該判定述語集合に対応するレコードセットの識別子で特定されるレコードセットのレコード長に設定するレコード長決定手段として機能させるものである。
【００２１】
また，前レコード長決定装置は，検査対象のソフトウェアの論理的仕様を、処理対象のレコードセットの識別子と判定条件に関する判定述語により定義した述語を記憶するプロパティ記憶手段と，前記プロパティ記憶手段から，レコード長に関する制約を有する述語を抽出して述語一覧記憶部に記憶する手段と，前記述語一覧記憶部に記憶された各述語について、充足可能性判定に必要な最短レコード長を特定する述語毎最短レコード長抽出手段と，前記プロパティ記憶手段に記憶された前記述語に含まれる前記判定述語を、前記レコードセットの識別子ごとにまとめた判定述語集合を生成する判定述語抽出手段と，前記判定述語抽出手段で生成された前記判定述語集合に基づいて生成した論理式により、該判定述語集合の充足可能性を判定する判定手段と，前記判定手段において，判定述語集合が充足可能であると判定された場合に，当該判定述語集合を構成する各判定述語に対応する各述語の前記最短レコード長を抽出し，抽出した各最短レコード長のうちの最長値を，当該判定述語集合に対応するレコードセットの識別子で特定されるレコードセットのレコード長に設定するレコード長決定手段を備える。
【発明の効果】
【００２２】
上記したプログラムまたは装置が実現する処理機能によれば，ソフトウェアが扱う可変長データ構造を有するレコードセットのレコード長を最適な長さで固定化することができる。よって，可変長データを扱うソフトウェアのプロパティ整合性判定処理にＳＭＴソルバを適用することが可能となる。
【図面の簡単な説明】
【００２３】
【図１】プロパティ整合性判定装置およびレコード長決定装置の一実施形態における構成例を示す図である。
【図２】プロパティ記憶部に記憶されるプロパティの例を示す図である。
【図３】述語一覧記憶部に記憶される述語一覧の例を示す図である。
【図４】プロパティ述語テーブルの例を示す図である。
【図５】判定述語テーブルの例および判定述語テーブルに格納された判定述語が必要とするレコード数の関係を模式的に示す図である。
【図６】レコードセット長テーブルの例を示す図である。
【図７】レコードセット長テーブルの最短レコード長の設定例を示す図である。
【図８】充足チェックテーブルの例を示す図である。
【図９】充足チェックテーブルの充足可能性判定の結果の設定例を示す図である。
【図１０】充足可能と判定された部分集合について，特定した最短レコード長の最長値の設定例を示す図である。
【図１１】充足可能な部分集合とその補集合の組み合わせ例を示す図である。
【図１２】判定述語集合を構成する部分集合および補集合を示す述語集合と，対応する組み合わせにおける必要レコード長の例を示す図である。
【図１３】充足チェックテーブルの長さ（必要レコード長）の設定例を示す図である。
【図１４】レコードセット長テーブルの最短レコード長の設定例を示す図である。
【図１５】コード生成におけるレコードセット"Ｂ情報Ｔ"の定義例を示す図である。
【図１６】コード生成におけるレコードセット"Ｂ情報Ｔ"用の関数の定義例を示す図である。
【図１７】プロパティ整合性判定装置およびレコード長決定装置のより詳細な構成例を示す図である。
【図１８】レコード長決定装置の述語毎採点レコード長抽出器の処理フロー図である。
【図１９】レコード長決定装置の判定述語抽出器の処理フロー図である。
【図２０】レコード長決定装置の判定述語抽出器の処理フロー図である。
【図２１】レコード長決定装置のレコード長決定器の処理フロー図である。
【図２２】レコード長決定装置のレコード長決定器の処理フロー図である。
【発明を実施するための形態】
【００２４】
図１は，本願で開示されるプロパティ整合性判定装置１およびレコード長決定装置１０の一実施形態における構成例を示す図である。
【００２５】
プロパティ整合性判定装置１は，ＳＭＴソルバの機能を有して，検証対象ソフトウェアのプロパティの整合性を判定する装置である。
【００２６】
プロパティ整合性判定装置１は，レコード長決定装置１０およびレコード生成器５を有する。レコード長決定装置１０は，プロパティ内の可変長データセットのレコード長を固定化するための最適なデータ長を設定する装置である。本実施形態において，レコード長決定装置１０は，プロパティ整合性判定装置１の内部に設けらるが，プロパティ整合性判定装置１の外部に設けるようにしてもよい。
【００２７】
レコード長決定装置１０は，プロパティ記憶部１１，述語一覧記憶部１２，述語毎最短レコード長抽出器２，判定述語抽出器３，およびレコード長決定器４を有する。
【００２８】
レコード長決定装置１０のプロパティ記憶部１１は，検証対象のソフトウェアの論理的仕様を定める情報であるプロパティを記憶する記憶部である。
【００２９】
図２は，プロパティ記憶部１１に記憶されるプロパティの例を示す図である。
【００３０】
本実施形態において，プロパティは，検証対象のソフトウェアの事前条件部分として，７つの事前条件（Ｐ１＿ＰＲＥ〜Ｐ７＿ＰＲＥ）が設定されているとする。
【００３１】
図２のプロパティが含む，関数ｆｉｌｔｅｒは，レコードセット（レコードの集合）と判定述語を引数として，判定関数を満たすレコードのみのレコードセットを返却し，関数ｎｕｍＯｆは，レコードセットを引数として，レコードセットの長さ（レコード長、すなわちレコードの数）を返却する。
【００３２】
関数ｅｘｉｓｔは，１以上のレコードが存在するレコードセットを返却し，「ｎｕｍＯｆ（…）＞＝１」とみなしている。
【００３３】
述語一覧記憶部１２は，検証対象のソフトウェアを記述する言語における述語のうち，レコード長に関する制約を示す述語を示す述語一覧を記憶する記憶部である。
【００３４】
図３は，述語一覧記憶部１２の例を示す図である。述語一覧記憶部１２は，検証対象のソフトウェアの言語に対応して用意され，処理要素数（例えばレコード数）に関連する定義を記述する述語の一覧を示す述語一覧テーブルを記憶する。
【００３５】
本実施例では，述語一覧記憶部１２の述語一覧は，レコードセット長に関連する関数として，“ｅｘｉｓｔ”，“ｎｕｍＯｆ”を含むものとする。
【００３６】
述語毎最短レコード長抽出器２は，プロパティ記憶部１１が記憶するプロパティから，述語一覧記憶部１２に該当する述語を抽出する処理と，抽出した述語を満たすレコード長の最短値を示す最短レコード長を特定する処理とを行う。
【００３７】
判定述語抽出器３は，述語毎最短レコード長抽出器２によって抽出された述語から，その述語が処理するレコードセットと判定条件を定める判定述語とを抽出する処理と，抽出したレコードセットごとに，抽出した判定述語をまとめて判定述語集合を生成する処理とを行う。
【００３８】
レコード長決定器４は，判定述語抽出器３によって生成された判定述語集合の充足可能性を判定する処理と，充足可能性の判定処理の結果にもとづいて，判定述語集合に対応するレコードセットのレコード長を算出する処理とを行う。
【００３９】
また，レコード長決定器４は，判定述語集合が充足可能である場合に，その判定述語集合を構成する各判定述語に対応する述語の最短レコード長を抽出して，抽出した最短レコード長の最長値を，レコードセットのレコード長に設定する処理を行うことができる。
【００４０】
また，レコード長決定器４は，判定述語集合が充足不能である場合に，その判定述語集合を構成する各判定述語に対応する述語の最短レコード長を抽出して，抽出した最短レコード長の総和を，レコードセットのレコード長に設定する処理を行うことができる。
【００４１】
また，レコード長決定器４は，判定述語集合が充足不能である場合に，その判定述語集合のべき集合を生成して，生成した空集合を除く部分集合各々の充足可能性を判定する処理と，判定述語集合を構成する部分集合の組み合わせを生成する処理と，部分集合の充足可能性の判定結果をもとに，生成した部分集合の組み合わせから，構成する部分集合が全て充足可能である組み合わせを抽出する処理と，抽出された組み合わせについて，その組み合わせを構成する部分集合各々について，部分集合を構成する判定述語に対応する述語の最短レコード長を抽出して，抽出した最短レコード長の最長値を求め，求めた最長値の総和を組み合わせの必要レコード長とする処理と，組み合わせの必要レコード長のうち最短値を，レコードセットのレコード長に設定する処理とを行うことができる。
【００４２】
さらに，レコード長決定器４は，前記生成した組み合わせから，構成する部分集合が全て充足可能である組み合わせが抽出されなかった場合に，生成した組み合わせ各々について，充足可能な部分集合を構成する判定述語に対応する述語の最短レコード長のうちの最長値を求める処理と，充足不能な部分集合を構成する判定述語に対応する述語の最短レコード長の総和を求める処理と，求めた最長値と総和との合計を，組み合わせの必要レコード長とする処理とを行うことができる。
【００４３】
プロパティ整合性判定装置１のコード生成器５は，プロパティに対応する充足可能性判定処理用のコードを生成した場合に，前記レコード長決定器によって設定されたレコード長を用いて前記レコードセットに関連する定義を生成する処理を行う。
【００４４】
次に，レコード長決定装置１０の処理動作を概説する。
【００４５】
レコード長決定装置１０の述語毎最短レコード長抽出器２は，プロパティ記憶部１１のプロパティから，述語一覧記憶部１２の述語一覧（以下，単に述語一覧テーブル１２という）に該当する述語を抽出して，抽出した述語を満たすレコード長の最短値を示す最短レコード長を特定する。述語毎最短レコード長抽出器２は，抽出した述語とその最短レコード長とをプロパティ述語テーブル１３に格納する。
【００４６】
図４は，プロパティ述語テーブル１３の例を示す図である。
【００４７】
プロパティ述語テーブル１３は，各述語を識別する情報である「識別情報（ＰＩＤ）」，プロパティから抽出した述語の定義の記述本体である「定義本体」，述語を満たす最小のレコード数を示す「最短レコード長」のデータ項目を含む。
【００４８】
図４のプロパティ述語テーブル１３において，“ＰＲＥＤ０１”の述語は，定義本体が“ｅｘｉｓｔ（Ａ情報Ｔ，Ａ情報．ｅｌｅ＿ａ１＞０ａｎｄＡ情報．ｅｌｅ＿ａ１＜１０）”であり，この述語の定義から特定された最短レコード長が“１”であることを示す。
【００４９】
また，“ＰＲＥＤ０３”の述語は，定義本体が“ｎｕｍＯｆ（ｆｉｌｔｅｒ（Ａ情報Ｔ，Ａ情報．ｅｌｅ＿ａ１＝＝５））＞＝５”であり，この述語の定義から特定された最短レコード長が“５”であることを示す。
【００５０】
判定述語抽出器３は，プロパティ述語テーブル１３に格納された述語から，その述語が処理するレコードセットと判定条件を定める判定述語とを抽出して，各述語から抽出した判定述語とレコードセットとを判定述語テーブル１４に格納する。
【００５１】
図５は，判定述語テーブル１４の例を示す図である。
【００５２】
図５（Ａ）に示す判定述語テーブル１４は，判定述語を識別する情報である「識別情報（ＪＩＤ）」，プロパティの述語から抽出された判定述語の識別情報である「識別情報（ＰＩＤ）」，プロパティの述語から抽出された判定述語の定義本体である「定義本体」，プロパティの述語から抽出されたレコードセットを示す「レコードセット」のデータ項目を含む。
【００５３】
図５（Ａ）の判定述語テーブル１４において，“Ｊ０１”の判定述語は，“ＰＲＥＤ０１”であるプロパティの述語に対応し，判定述語の定義本体が“Ａ情報．ｅｌｅ＿ａ１＞０ａｎｄＡ情報．ｅｌｅ＿ａ１＜１０”であり，レコードセットが“Ａ情報Ｔ”であることを示す。
【００５４】
図５（Ｂ）は，図５（Ａ）の判定述語テーブル１４に格納された判定述語がとりうるレコード数の範囲を模式的に示す図である。
【００５５】
図５（Ｂ）において，“Ｊ０１”の判定述語が必要なレコード数ｎＪ０１は，“０＜ｎＪ０１＜１０”であることを示す。また，“Ｊ０２”の判定述語が必要なレコード数ｎＪ０２は“ｎＪ０２＝＝５”，“Ｊ０３”の判定述語が必要なレコード数ｎＪ０３は“ｎＪ０３＜＝８”であることを示す。
【００５６】
続いて，判定述語抽出器３は，判定述語テーブル１４の判定述語をレコードセットごとにまとめて判定述語集合を生成し，各レコードセットに対応する判定述語集合を構成する判定述語のリストをレコードセット長テーブル１５に格納する。
【００５７】
図６は，レコードセット長テーブル１５の例を示す図である。
【００５８】
レコードセット長テーブル１５は，レコードセットを識別する情報である「識別情報（ＲＩＤ）」，レコードセットの定義名を示す「レコードセット」，レコードセットに対応する判定述語集合の構成要素である判定述語の識別情報を示す「判定述語集合」，判定述語集合を構成する判定述語に対応する述語を満たすレコード数の最小値である「最短レコード長」のデータ項目を含む。
【００５９】
判定述語抽出器３は，判定述語テーブル１４から，“Ｒ０１”であるレコードセット“Ａ情報Ｔ”の判定述語集合が，“Ｊ０１，Ｊ０２，Ｊ０３，Ｊ０４，Ｊ０５”の５つの判定述語で構成されることを示す。また，“Ｒ０２”であるレコードセット“Ｂ情報Ｔ”の判定述語集合が“Ｊ０６，Ｊ０７”の２つの判定述語で構成されることを示す。
【００６０】
レコード長決定器４は，以下のいずれかの処理を行って，レコードセットに対応する判定述語集合をもとに，レコードセットのレコード長を求める。
【００６１】
〔第１のレコード長決定処理例〕
処理ＳＴ１０：レコード長決定器４は，各レコードセットの判定述語集合を構成する判定述語をＡＮＤ連結した論理式の充足可能性を判定する。判定処理は，既知のＳＭＴソルバが実施する処理機能を適用して行う。
【００６２】
処理ＳＴ１１：レコード長決定器４は，判定述語のＡＮＤ連結による論理式が充足可能であると判定した場合に，プロパティ述語テーブル１３から，判定述語集合を構成する各判定述語に対応する述語の最短レコード長を抽出して，抽出した最短レコード長の最大値（最長の最短レコード長）を，レコードセット長テーブル１５の「最短レコード長」へ格納する。
【００６３】
例えば，レコードセット“Ｂ情報Ｔ”について，判定述語集合の判定述語のＡＮＤ連結による論理式が充足可能であるとする。レコード長決定器４は，図４に示すプロパティ述語テーブル１３から，レコードセット“Ｂ情報Ｔ”の判定述語集合を構成する判定述語“Ｊ０６”に対応する述語“ＰＲＥＤ０２”の最短レコード長が“１”と判定述語“Ｊ０７”に対応する述語“ＰＲＥＤ０７”の最短レコード長が“５”とを抽出する。レコード長決定器４は，図７に示すように，抽出した最短レコード長の最大値（５）をレコードセット長テーブル１５のレコードセット“Ｂ情報Ｔ”の「最短レコード長」へ格納する。
【００６４】
処理ＳＴ１２：レコード長決定器４は，判定述語集合の判定述語のＡＮＤ連結による論理式が充足不能であると判定した場合に，プロパティ述語テーブル１３から，判定述語集合を構成する各判定述語に対応する述語の最短レコード長を抽出して，抽出した最短レコード長の総和を，レコードセット長テーブル１５の「最短レコード長」に設定する。
【００６５】
例えば，レコードセット“Ａ情報Ｔ”について，判定述語集合の判定述語のＡＮＤ連結による論理式が充足不能であるとする。
【００６６】
レコード長決定器４は，図４に示すプロパティ述語テーブル１３から，レコードセット“Ａ情報Ｔ”の判定述語集合を構成する判定述語“Ｊ０１”に対応する述語“ＰＲＥＤ０１”の最短レコード長“１”，判定述語“Ｊ０２”に対応する述語“ＰＲＥＤ０３”の最短レコード長“５”，判定述語“Ｊ０３”に対応する述語“ＰＲＥＤ０４”の最短レコード長“１０”，判定述語“Ｊ０４”に対応する述語“ＰＲＥＤ０５”の最短レコード長“３”，判定述語“Ｊ０５”に対応する述語“ＰＲＥＤ０６”の最短レコード長“２５”を抽出する。そして，レコード長決定器４は，図７に示すように，抽出した最短レコード長の総和（１＋５＋１０＋３＋２５＝４４）を計算し，総和“４４”を，レコードセット長テーブル１５のレコードセット“Ａ情報Ｔ”の「最短レコード長」へ格納する。
【００６７】
このようにして，レコードセット毎に充足可能性判定に必要な最短レコード長を決定することができるため，可変長のテーブルを含むソフトウェアのプロパティ整合性判定処理を，ＳＭＴソルバを適用して行うことが可能となる。
【００６８】
〔第２のレコード長決定処理例〕
処理ＳＴ２０：レコード長決定器４は，次のようにしてレコード長を決定することも可能である。すなわち、判定述語集合を構成する判定述語をＡＮＤ連結した論理式が充足不能である場合に，判定述語集合を構成要素からべき集合を生成して，生成した空集合以外の部分集合（判定述語の集合）を充足チェックテーブル１６に格納する。
【００６９】
例えば，レコード長決定器４は，図６のレコードセット長テーブル１５のレコードセット“Ａ情報Ｔ”の判定述語集合の要素である判定述語｛Ｊ０１，Ｊ０２，Ｊ０３，Ｊ０４，Ｊ０５｝からべき集合を生成し，生成した部分集合に識別情報を付与して充足チェックテーブル１６に格納する。
【００７０】
図８は，充足チェックテーブル１６の例を示す図である。
【００７１】
充足チェックテーブル１６は，部分集合を識別する情報である「識別情報（ＩＤ）」，部分集合を構成する判定述語を示す「定義本体」，充足可能性判定結果を示す「充足可能性」，充足可能な部分集合を構成する各判定述語に対応する述語の最短レコード長の最大値（最長値）を示す「長さ」のデータ項目を含む。
【００７２】
図８の充足チェックテーブル１６において，“ＪＳ０１”の部分集合は，判定述語Ｊ０１，Ｊ０２，Ｊ０３，Ｊ０４，Ｊ０５で構成されることを示し，“ＪＳ０３”の部分集合は，判定述語Ｊ０１，Ｊ０２，Ｊ０３，Ｊ０５で構成されることを示す。
【００７３】
なお，本処理例において，レコード長決定器４は，再帰的な呼び出し手順によって実行される毎に補集合のべき集合を生成して，充足チェックテーブル１６に格納する。
【００７４】
処理ＳＴ２１：レコード長決定器４は，生成した部分集合について，部分集合を構成する判定述語のＡＮＤ連結による論理式の充足可能性を判定して，判定結果（“充足可能”または“充足不能”）を充足チェックテーブル１６に格納する。
【００７５】
図９は，判定結果および，充足可能と判定された部分集合の最短レコード長の最長値を格納した充足チェックテーブル１６の例を示す。
【００７６】
図９に示す充足チェックテーブル１６において，ＪＳ０７，ＪＳ１７，ＪＳ１８，ＪＳ２１，ＪＳ２６〜ＪＳ３１の部分集合が“充足可能”であると判定されたことを示す。
【００７７】
処理ＳＴ２２：レコード長決定器４は，充足可能な部分集合について，プロパティ述語テーブル１３を参照して，その部分集合を構成する各判定述語に対応する述語の最短レコード長を抽出し，抽出した最短レコード長の最長値を特定する。
【００７８】
図１０は，充足可能と判定された各部分集合について，特定した最短レコード長の最長値を示す図である。
【００７９】
レコード長決定器４は，例えば，部分集合“ＪＳ０７”について，部分集合を構成する判定述語“Ｊ０１，Ｊ０２，Ｊ０３”に対応する述語“ＰＲＥＤ０１，ＰＲＥＤ０３，ＰＲＥＤ０４”の各最短レコード長（１，５，１０）から，最長値“１０”を特定する。
【００８０】
また，レコード長決定器４は，部分集合“ＪＳ１７”について，部分集合を構成する判定述語“Ｊ０１，Ｊ０２”に対応する述語“ＰＲＥＤ０１，ＰＲＥＤ０３の各最短レコード長（１，５）から，最長値“５”を特定する。
【００８１】
処理ＳＴ２３：レコード長決定器４は，充足チェックテーブル１６から，“充足可能”が設定された部分集合を抽出し，その部分集合の補集合（判定述語の集合）を特定する。
【００８２】
図１１は，充足可能な部分集合とその補集合とを示す図である。
【００８３】
図１１に示す補集合“ＪＳ０７’”は，部分集合“ＪＳ０７”の補集合であって，判定述語Ｊ０４，Ｊ０５が要素であることを示す。同様に，補集合“ＪＳ１７’”は，部分集合“ＪＳ１７”の補集合であって，判定述語Ｊ０３，Ｊ０４，Ｊ０５が要素であることを示す。さらに，補集合“ＪＳ１８’”〜“ＪＳ３１’”も，それぞれ，部分集合“ＪＳ１８”〜“ＪＳ３１”の補集合であることを表す。
【００８４】
処理ＳＴ２４：レコード長決定器４は，充足チェックテーブル１６を参照して，各部分集合の補集合である部分集合の充足可能性を調べる。
【００８５】
レコード長決定器４は，図１１の各補集合のうち，補集合“ＪＳ０７’（“Ｊ２６”に相当）”，“ＪＳ２６’（“Ｊ０７”に相当）”が充足可能であり，他の補集合“ＪＳ１７’等が充足不能であることを調べる。
【００８６】
処理ＳＴ２５：レコード長決定器４は，判定述語集合を構成する部分集合が，充足可能な部分集合と，充足可能な補集合との組み合わせとなるものについて，必要レコード長を計算する。
【００８７】
レコード長決定器４は，処理ＳＴ２２で求めた部分集合“ＪＳ０７”に対応する述語の最短レコード長の最短値（１０）と，補集合“ＪＳ０７’” に対応する述語の最短レコード長の最短値（２５）との総和（３５）を，部分集合“ＪＳ０７”の組み合わせの必要レコード長として，充足チェックテーブル１６の部分集合“ＪＳ０７”の「長さ」に格納する。
【００８８】
同様に，レコード長決定器４は，処理ＳＴ２２で求めた部分集合“ＪＳ２６”に対応する述語の最短レコード長の最短値（２５）と，補集合“ＪＳ２６’” に対応する述語の最短レコード長の最短値（１０）との総和（３５）を，部分集合“ＪＳ２６”の組み合わせの必要レコード長として，充足チェックテーブル１６の部分集合“ＪＳ２６”の「長さ」に格納する。
【００８９】
レコード長決定器４は，充足不能である補集合が存在する場合に，処理ＳＴ２０〜Ｓ２５の処理を繰り返し，その補集合のべき集合を生成して，生成した補集合を構成する部分集合に対して，充足可能性を判定して，最短レコード長の最長値を求め，その部分集合の組み合わせの必要レコード長を計算する。
【００９０】
このように，レコード長決定器４が，判定述語集合のべき集合の生成と，生成した各部分集合の充足不能な補集合を対象とする再帰的処理を行うことによって，判定述語集合を構成する部分集合が全て充足可能である組み合わせを特定して，その組み合わせの必要レコード長を求めることができる。
【００９１】
図１２は，判定述語集合を構成する部分集合および補集合を示す述語集合と，対応する組み合わせにおける必要レコード長の例を示す図である。
【００９２】
図１２において，“ＪＳ０７”の組み合わせを示す“ＪＳ０７＝｛１，２，３｝，｛４，５｝”は，部分集合“ＪＳ０７”と補集合“ＪＳ０７’”それぞれに含まれる述語を示す。｛１，２，３｝は，｛Ｊ０１，Ｊ０２，Ｊ０３｝を表し，｛４，５｝は，｛Ｊ｝０４，Ｊ０５｝を表す。
【００９３】
“ＪＳ０７”の長さは，“ＪＳ０７”の組み合わせの必要レコード長であり，“ＪＳ０７”の最長値（１０）＋“ＪＳ０７’”の最長値（２５）の総和“３５”であることを示す。
【００９４】
また，部分集合“ＪＳ１７”の組み合わせは，部分集合“ＪＳ１７＝｛１，２｝”と，補集合“ＪＳ０７’”の組み合わせであり，補集合“ＪＳ０７’は，さらに“ＪＳ２６”と“ＪＳ２９”との組み合わせであることを示す。
【００９５】
したがって，部分集合“ＪＳ１７”の組み合わせの必要レコード長は，“ＪＳ１７”の最長値（５）＋“ＪＳ０７’”の最長値（３５＝“ＪＳ２６”の最長値（２５）＋“ＪＳ２９”の最長値（１０））の総和“４０”であることを示す。
【００９６】
図１３は，上記の処理ＳＴ２０〜Ｓ２５の繰り返しにより，充足可能な部分集合による組み合わせの必要レコード長が設定された充足チェックテーブル１６の例を示す図である。
【００９７】
処理ＳＴ２６：レコード長決定器４は，充足チェックテーブル１６に設定した各組み合わせの「長さ（必要レコード長）」から，最小値（最短レコード長）を特定して，レコードセット長テーブル１５の最短レコード長に格納する。
【００９８】
図１３に示すように，充足チェックテーブル１６において，レコードセット“Ａ情報Ｔ”の判定述語集合の各組み合わせの「長さ（必要レコード長）」として“３５”〜“４０”の値が格納されているので，レコード長決定器４は，最小値“３５”を特定して，図１４に示すように，レコードセット長テーブル１５のレコードセット“Ａ情報Ｔ”の最短レコード長に“３５”を格納する。
【００９９】
以上のように第２のレコード長決定処理では，判定述語集合を，充足可能な要素（判定述語）のみで構成されるような組み合わせを特定し，その組み合わせにおいて必要レコード長が最小となる場合の値を求めることができる。よって，レコードセットのレコード長を，より短いレコード長で設定することが可能となり，処理負担を抑制できる適切なレコード長によるレコードセットの固定化を実現することができる。
【０１００】
続いて，コード生成器５は，プロパティ整合性判定処理を実行するＳＭＴソルバに適用可能なコード生成処理において，第１または第２のレコード長決定処理によって最短レコード長が設定されたレコードセット長テーブル１５を参照して，各レコードセットのレコード長を設定する。
【０１０１】
図１５は，レコードセット“Ｂ情報Ｔ”の定義例を示す図である。
【０１０２】
図１５に示す定義例は，レコードセット“Ｂ情報Ｔ”（ＢＩｎｆｏＲｅｃｏｒｄＳｅｔ）を固定長＝５のレコードセットとする定義を，Ｙｉｃｅｓと呼ばれるＳＭＴソルバが処理可能な入力言語によって記述した例である。この記述例では，“Ｂ情報Ｔ”のレコードセットは，“Ｒｅｃｏｒｄ＿Ｂｉｎｆｏ”というレコードの５つの組として定義されている。
【０１０３】
図１６は，レコードセット“Ｂ情報Ｔ”用の関数の定義例を示す図である。
【０１０４】
図１６の定義例では，レコードセット“Ｂ情報Ｔ”用のｅｘｉｓｔ関数（ｅｘｉｓｔ＿Ｂｉｎｆｏ）のレコードの処理部分を固定化した定義を，Ｙｉｃｅｓと呼ばれるＳＭＴソルバが処理可能な入力言語によって記述した例である。この記述例では，ｅｘｉｓｔ関数の処理部分が，長さ“５”のレコードセットに対する処理として定義されている。
【０１０５】
このように，検証対象のプログラムが可変長レコードを含む場合でも，可変長レコードを固定化するために適切なレコード長を決定してＳＭＴソルバが処理可能なコードを生成することができるため，プロパティ整合性判定処理に，ＳＭＴソルバを適用することが可能となる。
【０１０６】
図１７は，図１に示すプロパティ整合性判定装置１およびレコード長決定装置１０の一実施形態におけるより詳細な構成例を示す図である。図１７に示すプロパティ整合性判定装置１は，レコード長決定装置１０およびコード生成器５０を備える。
【０１０７】
レコード長決定装置１０は，プロパティ記憶部１１，述語一覧記憶部（述語一覧テーブル）１２，プロパティ述語テーブル１３，判定述語テーブル１４，レコードセット長テーブル１５，充足チェックテーブル１６，述語毎最短レコード長抽出器２０，判定述語抽出器３０，およびレコード長決定器４０を備える。
【０１０８】
レコード長決定装置１０のプロパティ記憶部１１は，図１に示すプロパティ記憶部と同様であり，図２に示すプロパティを記憶する。
【０１０９】
述語一覧記憶部（述語一覧テーブル）１２は，図１に示す述語一覧記憶部１２と同様であり，図３に示す述語一覧を記憶する。
【０１１０】
プロパティ述語テーブル１３は，述語毎最短長レコード抽出器２０の述語抽出部２１によって生成され，図４に示すデータが格納される。
【０１１１】
判定述語テーブル１４は，判定述語抽出器３０の判定述語抽出部３１によって生成され，図５に示すデータが格納される。
【０１１２】
レコードセット長テーブル１５は，判定述語抽出器３０の判定述語集合生成部３２によって生成され，図６に示すデータが格納される。
【０１１３】
充足チェックテーブル１６は，レコード長決定器４０の充足可能性判定部４１によって生成され，図８に示すデータが格納される。
【０１１４】
述語毎最短レコード長抽出器２０は，プロパティ記憶部１１に記憶されたプロパティから，述語一覧テーブル１２に該当する述語を抽出する述語抽出部２１と，述語抽出部２１が抽出した述語を満たすレコード長の最小値（最短値）を示す最短レコード長を特定する最短長計算部２２とを備える。
【０１１５】
判定述語抽出器３０は，述語抽出部２１によって抽出された述語から，その述語が処理するレコードセットと判定条件を定める判定述語とを抽出する判定述語抽出部３１と，判定述語抽出部３１が抽出したレコードセットごとに，抽出した判定述語をまとめて判定述語集合を生成する判定述語集合生成部３２とを備える。
【０１１６】
レコード長決定器４は，判定述語集合生成部３２によって生成された判定述語集合の充足可能性を判定する充足可能性判定部４１と，充足可能性判定部４１が行った充足可能性判定の判定結果にもとづいて，判定述語集合に対応するレコードセットのレコード長を算出するレコード長計算部４２とを備える。
【０１１７】
プロパティ整合性判定装置１のコード生成器５０は，図１に示すコード生成器５と同様である。
【０１１８】
図１８〜図２２は，レコード長決定装置１０の述語毎最短レコード長抽出器２０，判定述語抽出器３０，およびレコード長決定器４０の処理の処理フロー図である。
【０１１９】
述語毎最短レコード長抽出器２０の述語抽出部２１は，プロパティ記憶部１１に処理すべきプロパティが残っているかを判定する（ステップＳ１）。処理すべきプロパティが残っていれば（ステップＳ１のＹ），述語抽出部２１は，プロパティ内に述語一覧テーブル１２にマッチする述語があるかを判定する（ステップＳ２）。述語一覧テーブル１２にマッチする述語があれば（ステップＳ２のＹ），述語抽出部２１は，マッチした述語を抽出し，プロパティ述語テーブル１３に格納する（ステップＳ３）。
【０１２０】
述語一覧テーブル１２にマッチする述語がなければ（ステップＳ２のＮ），ステップＳ１の処理へ戻る。そして，処理すべきプロパティが残っていなければ（ステップＳ１のＮ），ステップＳ４の処理へ進む。
【０１２１】
述語毎最短レコード長抽出器２０の最短長計算部２２は，プロパティ述語テーブル１３内に処理すべき述語が残っているかを判定する（ステップＳ４）。処理すべき述語が残っていれば（ステップＳ４のＹ），最短長計算部２２は，不等式等の述語から，述語を満たす最短レコード長を求めて，プロパティ述語テーブル１３に格納する（ステップＳ５）。
【０１２２】
処理すべき述語が残っていなければ（ステップＳ４のＮ），ステップＳ１１の処理へ進む。
【０１２３】
判定述語抽出器３０の判定述語抽出部３１は，プロパティ述語テーブル１３内に処理すべき述語が残っているかを判定する（ステップＳ１１）。処理すべき述語が残っていれば（ステップＳ１１のＹ），判定述語抽出部３１は，述語内の判定述語と対応するレコードセットを抽出し，判定述語テーブル１４に格納する（ステップＳ１２）。処理すべき判定述語が残っていなければ（ステップＳ１１のＮ），ステップＳ１３の処理へ進む。
【０１２４】
判定述語抽出部３１は，述語内の判定述語と対応するレコードセットを抽出し，判定述語テーブル１４に格納する（ステップＳ１２）。
【０１２５】
次に，判定述語抽出器３０の判定述語集合生成部３２は，判定述語テーブル１４内に処理すべき判定述語が残っているかを判定する（ステップＳ１３）。処理すべき判定述語が残っていれば（ステップＳ１３のＹ），判定述語集合生成部３２は，対応する判定述語のレコードセットが既にレコードセット長テーブル１５に格納されているかを判定する（ステップＳ１４）。
【０１２６】
対応する判定述語のレコードセットがレコードセット長テーブル１５に格納されていれば（ステップＳ１４のＹ），判定述語集合生成部３２は，レコードセット長テーブル１５内の対応するレコードセットに判定述語を追加する（ステップＳ１５）。対応する判定述語のレコードセットがレコードセット長テーブル１５に格納されていなければ（ステップＳ１４のＮ），判定述語集合生成部３２は，レコードセット長テーブル１５に，新たにレコードセットを追加して，対応する判定述語を格納する（ステップＳ１６）。
【０１２７】
続いて，レコード長決定器４０は，レコードセット長テーブル１５内に処理すべきレコードが残っているかを判定する（ステップＳ２１）。レコードセット長テーブル１５内に処理すべきレコードが残っていれば（ステップＳ２１のＹ），レコード長決定器４０は，レコードセット長テーブル１５の判定述語の集合を引数として，レコード長計算処理を行い（ステップＳ２２），レコード長計算結果をレコードセット長テーブル１５に格納する（ステップＳ２３）。レコード長決定器４０は，処理すべきレコードが残っていなければ（ステップＳ２１のＮ）処理を終了する。
【０１２８】
図２１および図２２に示す処理フローのステップＳ２２０〜Ｓ２２６，Ｓ２３０〜Ｓ２３５は，図２０に示すステップＳ２２のレコード長計算処理の詳細な処理フローである。
【０１２９】
レコード長決定器４０の充足可能性判定部４１は，レコードセット長テーブル１５のレコードセットの判定述語集合を引数として，判定述語をＡＮＤ連結した論理式が充足可能であるかを判定する（ステップＳ２２０）。判定述語をＡＮＤ連結した論理式が充足可能であれば（ステップＳ２２０のＹ），レコード長計算部４２は，判定述語テーブル１４とプロパティ述語テーブル１３とを参照して，各判定述語の最短レコード長を求め，そのうち最長のレコード値（最大値）を返却する（ステップＳ２２１）。
【０１３０】
判定述語をＡＮＤ連結した論理式が充足可能でなければ（ステップＳ２２０のＮ），レコード長決定器４０は，判定述語集合のべき集合（空集合以外の子集合）を生成し，生成した部分集合（判定述語の集合）を充足チェックテーブル１６に格納する（ステップＳ２２２）。
【０１３１】
レコード長決定器４は，処理すべき部分集合（判定述語の集合）が残っているかを判定する（ステップＳ２２３）。処理すべき部分集合が残っていれば（ステップＳ２２３のＹ），充足可能性判定部４１は，判定述語をＡＮＤ連結した論理式の充足可能性を調べ，その結果（“充足可能”ｏｒ“充足不能”）を充足チェックテーブル１６に格納する（ステップＳ２２４）。
【０１３２】
処理すべき判定述語の集合が残っていなければ（ステップＳ２２３のＮ），レコード長決定器４０は，充足チェックテーブル１６内の判定結果が全て“充足不能”であるかを調べる（ステップＳ２２５）。充足チェックテーブル１６内の判定結果が全て“充足不能”であれば（ステップＳ２２５のＹ），レコード長計算部４２は，判定述語テーブル１４とプロパティ述語テーブル１３とを参照して，各判定述語の最短レコード長を求め，その総和を返却する（ステップＳ２２６）。
【０１３３】
充足チェックテーブル１６内の判定結果が全て“充足不能”でなければ（ステップＳ２２５のＮ），レコード長決定器４０は，充足チェックテーブル１６内に処理すべき判定述語の集合が残っているかを判定する（ステップＳ２３０）。充足チェックテーブル１６内に処理すべき判定述語の集合が残っていれば（ステップＳ２３０のＹ），充足可能性判定部４１は，判定述語の集合の結果が“充足可能”であるかを調べる（ステップＳ２３１）。判定述語の集合の結果が“充足可能”であれば（ステップＳ２３１のＹ），レコード長決定器４０は，判定述語の集合として選択されている述語の集合の補集合を生成する（ステップＳ２３２）。レコード長決定器４０は，ステップＳ２２のレコード長計算処理の手続の再帰的呼び出しを行って，ステップＳ２３２で生成した補集合を引数としてレコード長計算処理を行う（ステップＳ２３３）。
【０１３４】
レコード長計算部４２は，ステップＳ２３３の処理の結果として，判定述語の集合から選択された述語集合内の述語の最長の最短レコード長に，ステップＳ２３２の処理でのレコード長を加算した値を，充足チェックテーブル内に格納する（ステップＳ２３４）。
【０１３５】
充足チェックテーブル１６内に処理すべき判定述語の集合が残っていなければ（ステップＳ２３０のＮ），レコード長計算部４２は，充足チェックテーブル１６内の最小の“長さ”を返却して（ステップＳ２３５），処理を終了する。
【０１３６】
以上説明したプロパティ整合性判定装置１およびレコード長決定装置１０の処理機能は，コンピュータによって実現することができる。その場合，プロパティ整合性判定装置１およびレコード長決定装置１０が有すべき機能の処理内容を記述したプログラムが提供される。そのプログラムをコンピュータで実行することにより，上記説明した処理機能がコンピュータ上で実現される。
【０１３７】
プロパティ整合性判定装置１の処理内容を記述したプログラムは，コンピュータで読み取り可能な記録媒体に記録しておくことができる。
【０１３８】
プログラムを実行するコンピュータは，例えば，可搬型記録媒体に記録されたプログラムもしくはサーバコンピュータから転送されたプログラムを，自己の記憶装置に格納する。そして，コンピュータは，自己の記憶装置からプログラムを読み取り，プログラムに従った処理を実行する。なお，コンピュータは，可搬型記録媒体から直接プログラムを読み取り，そのプログラムに従った処理を実行することもできる。また，コンピュータは，サーバコンピュータからプログラムが転送されるごとに，逐次，受け取ったプログラムに従った処理を実行することもできる。
【０１３９】
プログラムを流通させる場合には，例えば，そのプログラムが記録されたＤＶＤ（Ｄｉｇｉｔａｌ  Ｖｅｒｓａｔｉｌｅ  Ｄｉｓｃ），ＣＤ−ＲＯＭ（Ｃｏｍｐａｃｔ  Ｄｉｓｃ  Ｒｅａｄ  Ｏｎｌｙ  Ｍｅｍｏｒｙ）などの可搬型記録媒体が販売される。また，プログラムをサーバコンピュータの記憶装置に格納しておき，ネットワークを介して，サーバコンピュータから他のコンピュータにそのプログラムを転送することもできる。
【符号の説明】
【０１４０】
１  プロパティ整合性判定装置
１０  レコード長決定装置
２，２０  述語毎最短レコード長抽出器
３，３０  判定述語抽出器
４，４０  レコード長決定器
５，５０  コード生成器
１１  プロパティ記憶部
１２  述語一覧記憶部
１３  プロパティ述語テーブル
１４  判定述語テーブル
１５  レコードセット長テーブル
１６  充足チェックテーブル
【図１】
2011013797.tif 000003
【図２】
2011013797.tif 000004
【図３】
2011013797.tif 000005
【図４】
2011013797.tif 000006
【図５】
2011013797.tif 000007
【図６】
2011013797.tif 000008
【図７】
2011013797.tif 000009
【図８】
2011013797.tif 000010
【図９】
2011013797.tif 000011
【図１０】
2011013797.tif 000012
【図１１】
2011013797.tif 000013
【図１２】
2011013797.tif 000014
【図１３】
2011013797.tif 000015
【図１４】
2011013797.tif 000016
【図１５】
2011013797.tif 000017
【図１６】
2011013797.tif 000018
【図１７】
2011013797.tif 000019
【図１８】
2011013797.tif 000020
【図１９】
2011013797.tif 000021
【図２０】
2011013797.tif 000022
【図２１】
2011013797.tif 000023
【図２２】
2011013797.tif 000024