(57)【特許請求の範囲】
【請求項１】
論理型プログラムが入力される入力部、論理型プログラムを有限状態機械記述に変換するための変換部、変換された有限状態機械記述を比較するための比較部および表示装置を有する出力部を備える論理型プログラム比較装置で実行される論理型プログラム検証方法であって、
前記入力部において、各々が手続とデータ型のプログラム変数を含む２つの論理型プログラムを入力データとして受け付ける入力ステップと、
前記変換部において、前記各論理型プログラムを、前記各論理型プログラムの変数のデータ型を決定し、前記各論理型プログラムを選言形式の表現を含む完備形式に変換し、前記各論理型プログラム中の手続呼出を手続ボディに展開し、前記各論理型プログラムを遷移関数式からなる遷移関数に置き換える、という一連の処理に従って、その各々が内部状態、入力値、及び出力値を含む第１及び第２の有限状態機械記述にそれぞれ変換する変換ステップと、
前記比較部において、前記遷移関数を比較することにより、前記第１及び第２の有限状態機械記述の状態間、入力値間、及び出力値間に等価関係が存在するか否かを決定し、前記有限状態機械記述が、等価と考えられる全ての入力と等価と考えられる全ての状態に対して、等価と考えられる個々の出力を生ずるか否かを決定する比較ステップと、
前記出力部において、前記比較ステップの結果を出力する出力ステップと、
を有することを特徴とする論理型プログラム検証方法。
【請求項２】
前記入力ステップは、汎化質問を前記各論理型プログラムの一部として入力し、
前記変換ステップは、前記汎化質問に基づいて前記変換を行うことを特徴とする請求項１記載の論理型プログラム検証方法。
【請求項３】
前記変換ステップは、前記各論理型プログラムに静的解析を適用することによって前記データ型を決定するように構成されたことを特徴とする請求項１記載の論理型プログラム検証方法。
【請求項４】
前記比較ステップは、制約解法を用いて前記比較を行い、
この制約解法は、
入力、出力、または状態を表す各プログラム変数に固有の制約変数を割り当てるステップと、
前記第１の論理型プログラムから、特定のデータ型の各制約変数と、対応するデータ型の他の制約変数とがペアになるように制約変数をグループ化するステップと、
前記第２の論理型プログラムから、特定のデータ型の各制約変数と、対応するデータ型の他の制約変数とをペアになるように制約変数をグループ化するステップと、
前記制約変数の各ペア間の非等価関係の連言を生成するステップと、
選言形式の式について可能な全ての再配列に対して、個々の位置において生じる制約変数間に等価関係を生成するステップと、
前記ステップによって生成された前記非等価関係の連言と前記等価関係を新たな式に対する制約として設定するステップと、
前記制約を用いて前記新たな式を解くステップとを有することを特徴とする請求項１記載の論理型プログラム検証方法。
【請求項５】
前記各論理型プログラムは、述語論理の部分集合である確定節を組み合わせて記述され、各確定節は、質問、ルール、および事実のいずれかに限定されることを特徴とする請求項１記載の論理型プログラム検証方法。
【請求項６】
再帰的手続ボディを含む再帰的手続が、その再帰的手続ボディを反復表現にマッピングし、再帰的呼出を削除することによって、有限状態機械記述内にマッピングされることを特徴とする請求項１記載の論理型プログラム検証方法。
【請求項７】
前記変換ステップは、
前記遷移関数式を、共通値によって変数をグループ化するように並べ換え、各変数に固有コードを代入するステップと、
前記遷移関数式を、共通値によって変数をグループ化するように並べ換えるステップと、
前記遷移関数式において前記内部状態の１つが複数の値を持つ場合に、その遷移関数式を、前記１つの内部状態が各式において異なる値を持つような複数の式に変換するステップと、
固有の内部状態を含む各遷移関数式を固有コードによって符号化するステップとを有することを特徴とする請求項１記載の論理型プログラム検証方法。
【発明の詳細な説明】
【０００１】
【産業上の利用分野】
本発明は、双方が論理型プログラムの形式で表現された、システム仕様及びその仕様を具体化した実システムについて、両者を比較することによって、実システムの妥当性を検証する方法に関するものである。
【０００２】
【従来の技術】
コンピュータ・システムなど、ハードウェアやソフトウェアを含む各種システムは、一般に、まずその仕様が決定され、この仕様が実システムとして具体化される。ここで、「仕様」とは、システム設計者が具体化の際に満足すべきと考える条件を記述したものであり、一般に、曖昧さを残さずに記述されるが読みやすい。一方、この仕様の内容がソフトウェアやハードウェア上に具体化されたものが実システムであり、実システムの設計は、ソフトウェア的構成単位やハードウェア的構成単位による問題解決の手法が、その詳細に至るまで完全に表現できるような形式によって行われる。
【０００３】
そして、このようなシステム設計において「検証」とは、実システムを分析し、仕様の全ての部分が実システムによって満足されているか否かを決定することを意味する。そして、検証は、設計者の意図する所期の効果を奏するシステムを誤りなく実現する上で、不可欠な作業である。
【０００４】
そして、システムをハードウェア的に又はソフトウェア的に具体化する開発過程においても、開発されつつある実システムが、仕様の全ての部分を充足するか否かをできるかぎり確認することが望ましい。このような開発過程における検証は、システムの信頼性を向上させ、作業工程の後戻りを最小限にするために、極めて効果的である。
【０００５】
仕様で記述された要件を全て満足している実システムは、仕様を満足していると言われ、近年のシステムの大規模・複雑化という現況において、仕様の満足を確保することは、システム開発での極めて重要な課題に位置付けられている。
【０００６】
このような仕様の記述形式としては各種のものが知られており、検証の対象となる要件の種類に応じて、様々な形式の仕様が設計者によって用いられている。例えば、通信プロトコルのような非同期式システムについては、各イベントのタイミングに基づいて条件を表現する仕様が適しており、このような目的に対応した仕様記述言語を用いることが適している。このような言語の代表的なものは、例えば時相論理である。また、多くのハードウェアが属する同期式システムについては、ハードウェア的又はソフトウェア的構成要素を単位と考え、これら構成要素の入出力の関連に基づいて条件を表現する仕様が適している。本発明は、入出力に基づいてシステムの妥当性を検証するものであり、後者が主な適用対象である。
【０００７】
ある実システムにおけるこのような出力の妥当性を、所定の仕様に基づいて検証する手法の一つとしては、次のようなものが知られている。すなわち、実システムの内容とその仕様の双方を、有限状態機械（ｆｉｎｉｔｅ  ｓｔａｔｅ  ｍａｃｈｉｎｅ（ＦＳＭ））  に基づいた表現形式（以下、単に「ＦＳＭ」という。）に翻訳し、その上でこれら２つのＦＳＭを比較する手法である。ＦＳＭに翻訳すれば、仕様と実システムとの間に生じ得る文法上の相違、例えば、変数名などの相違が除去されるので、仕様と実システムの意味内容が共通の表現として提供される結果となり、両者の比較が容易なものとなる。
【０００８】
このＦＳＭは、それ自体、ブール式を用いて表現することが可能であるが、ＦＳＭはしばしば非常に大規模化する。このため、ブール式による表現は、さらに、二分岐決定ダイヤグラム（ｂｉｎａｒｙ  ｄｅｃｉｓｉｏｎ  ｄｉａｇｒａｍｓ（ＢＤＤｓ））によって表される場合もある。この二分岐決定ダイヤグラムは、ＦＳＭの内容を表すのみならず、組織化されたアルゴリズムの集合を提供するもので、このアルゴリズムは、大規模なブール式についても高速な処理を実現できるという利点を有する。
【０００９】
そして、２つのＦＳＭを比較するためには、ＦＳＭが基礎としている２つの有限状態機械が、同数の状態を有すると仮定することが一般的である。さらに、２つのＦＳＭの比較を有意義なものとするために、２つの有限状態機械が受け付ける入力の範囲も同一と仮定される。
【００１０】
２つのＦＳＭモデルの比較では、具体的には、有限状態機械の各状態において、２つの有限状態機械が、同一の入力に対して同一の出力を生成するか否かを検証する必要がある。この場合、２つの機械はそれぞれの初期状態からスタートすることになる。すなわち、２つの機械のあるカレント（現在の）状態が初期状態とされ、まず、このカレント状態について、２つの機械の相互に対応する出力が、あり得る全ての入力に対して同一か否かがチェックされる。この手順は、カレント状態から直接間接に到達可能な全ての状態に対して繰り返し実行され、全ての到達可能な状態がチェックされ尽くせば、２つのＦＳＭ全体の同一性を判定することができる。
【００１１】
【発明が解決しようとする課題】
ところで、上記のようなＢＤＤに基づいたＦＳＭモデル同士の比較は、コンピュータ上で非常に迅速に実行することができる。しかしながら、この手法で用いられるＢＤＤ自体の表現力は必ずしも豊かなものではなく、また、ＢＤＤによる表現は、各状態によって構成される状態空間内のパターンを直接利用して作成することができなかった。このため、いかに緻密なＢＤＤ表現を用いることができるか否かは、ブール式中のパターンを発見するユーザの能力に左右されざるを得なかった。さらに、ＢＤＤ表現の効率は、ブール式中で生じる変数の順序に大きく影響されるが、変数の理想的な順序を決定することも極めて困難であった。このため、ＦＳＭを用いた従来の手法では、効率的な妥当性の確認が困難であった。
【００１２】
また、従来のＦＳＭモデルに基づいた検証手法には、厳密に限定されている（ｆｉｎｉｔｅ：  有限な）状態機械（ｓｔａｔｅ  ｍａｃｈｉｎｅｓ）の比較しか行えないという欠点が存在していた。すなわち、実際のシステムの妥当性検証では、パラメータで表示された仕様や実システムを取り扱うことが望まれる場合も多い。しかし、そのような場合は、システムの構成の一部が不特定な変数として残されているため、従来の手法による検証は困難であった。例えば、スタックを用いる実システムをスタックを用いる仕様と比較する場合には、スタックの内容の詳細は不特定なパラメータとして残されていることが考えられる。従来の手法では、このような場合の妥当性検証は困難であった。
【００１３】
本発明は、上記のような従来技術の問題点を解決するために提案されたもので、その目的は、パラメータによる表示を含む論理型プログラムについても比較による妥当性検証が可能な論理型プログラム検証方法を提供することである。
【００１４】
また、本発明の他の目的は、検証に適した規則性にしたがって構成された規範的なＦＳＭを得ることができる論理型プログラム検証方法を提供することである。また、本発明の他の目的は、プログラムに基づいて各データ型を決定する煩雑な手数を省くことができる論理型プログラム検証方法を提供することである。また、本発明の他の目的は、より多様な装置の比較が可能で、また、比較全体を迅速・効率的に行う論理型プログラム検証方法を提供することである。また、本発明の他の目的は、状態の内部表現が相違する有限状態機械同士を比較することができる論理型プログラム検証方法を提供することである。また、本発明の他の目的は、従来の手法と比べてより高度の抽象が可能な論理型プログラム検証方法を提供することである。また、本発明の他の目的は、検証を効率的に実現する論理型プログラム検証方法を提供することである。
【００１５】
【課題を解決するための手段】
上記の目的を達するため、請求項１の論理型プログラム検証方法は、論理型プログラムを入力するための入力部、論理型プログラムを有限状態機械記述に変換するための変換部、変換された有限状態機械記述を比較するための比較部および表示装置を有する出力部を備える論理型プログラム比較装置で実行される論理型プログラム検証方法であって、前記入力部から、各々が手続とデータ型のプログラム変数を含む、２つの論理型プログラムを入力する入力ステップと、前記変換部において、前記各論理型プログラムを、前記各論理型プログラムの変数のデータ型を決定し、前記各論理型プログラムを選言形式の表現を含む完備形式に変換し、前記各論理型プログラム中の手続呼出を手続ボディに展開し、前記各論理型プログラムを遷移関数式からなる遷移関数に置き換える、という一連の処理に従って、その各々が内部状態、入力値、及び出力値を含む第１及び第２の有限状態機械記述にそれぞれ変換する変換ステップと、前記比較部において、前記遷移関数を比較することにより、前記第１及び第２の有限状態機械記述の状態間、入力値間、及び出力値間に等価関係が存在するか否かを決定し、前記有限状態機械記述が、等価と考えられる全ての入力と等価と考えられる全ての状態に対して、等価と考えられる個々の出力を生ずるか否かを決定する比較ステップと、前記出力部において、前記比較ステップの結果を出力する出力ステップと、を有することを特徴とする。
【００１６】
また、請求項２の発明は、請求項１記載の論理型プログラム検証方法において、前記入力ステップは、汎化質問を前記各論理型プログラムの一部として入力し、前記変換ステップは、前記汎化質問に基づいて前記変換を行うことを特徴とする。
【００１７】
また、請求項３の発明は、請求項１記載の論理型プログラム検証方法において、前記変換ステップは、前記各論理型プログラムに静的解析を適用することによって前記データ型を決定するように構成されたことを特徴とする。
【００１８】
また、請求項４の発明は、請求項１記載の論理型プログラム検証方法において、前記比較ステップは、制約解法を用いて前記比較を行い、この制約解法は、入力、出力、または状態を表す各プログラム変数に固有の制約変数を割り当てるステップと、前記第１の論理型プログラムから、特定のデータ型の各制約変数と、対応するデータ型の他の制約変数とがペアになるように制約変数をグループ化するステップと、前記第２の論理型プログラムから、特定のデータ型の各制約変数と、対応するデータ型の他の制約変数とをペアになるように制約変数をグループ化するステップと、前記制約変数の各ペア間の非等価関係の連言を生成するステップと、選言形式の式について可能な全ての再配列に対して、個々の位置において生じる制約変数間に等価関係を生成するステップと、前記ステップによって生成された前記非等価関係の連言と前記等価関係を新たな式に対する制約として設定するステップと、前記制約を用いて前記新たな式を解くステップとを有することを特徴とする。
【００１９】
また、請求項５の発明は、請求項１記載の論理型プログラム検証方法において、前記各論理型プログラムは、述語論理の部分集合である確定節を組み合わせて記述され、各確定節は、質問、ルール、および事実のいずれかに限定されることを特徴とする。
【００２０】
また、請求項６の発明は、請求項１記載の論理型プログラム検証方法において、再帰的手続ボディを含む再帰的手続が、その再帰的手続ボディを反復表現にマッピングし、再帰的呼出を削除することによって、有限状態機械記述内にマッピングされることを特徴とする。
【００２１】
また、請求項７の発明は、請求項１記載の論理型プログラム検証方法において、前記変換ステップは、前記遷移関数式を、共通値によって変数をグループ化するように並べ換え、各変数に固有コードを代入するステップと、前記遷移関数式を、共通値によって変数をグループ化するように並べ換えるステップと、前記遷移関数式において前記内部状態の１つが複数の値を持つ場合に、その遷移関数式を、前記１つの内部状態が各式において異なる値を持つような複数の式に変換するステップと、固有の内部状態を含む各遷移関数式を固有コードによって符号化するステップとを有することを特徴とする。
【００２２】
【作用】
上記のような構成を有する本発明は、次のような作用を有する。すなわち、請求項１の発明では、入力ステップによって、各々が手続とデータ型のプログラム変数を含む２つの論理型プログラムが入力され、入力された２つの論理型プログラムが、変換ステップによって、その各々が内部状態、入力値、及び出力値を含む、第１及び第２の有限状態機械記述に変換される。この変換ステップにおいては、各論理型プログラムの変数のデータ型が決定され、各論理型プログラムが選言（論理和）形式の表現を含む完備形式に変換され、各論理型プログラム中の手続呼出が手続ボディに展開され、各論理型プログラムが遷移関数式からなる遷移関数に置き換えられる。そして、比較ステップによって、遷移関数を比較することにより、第１及び第２の有限状態機械記述の状態間、入力値間、及び出力値間に等価関係が存在するか否かが決定され、有限状態機械記述が、等価と考えられる全ての入力と等価と考えられる全ての状態に対して、等価と考えられる個々の出力を生ずるか否かが決定される。この比較ステップの結果は、出力ステップによって出力される。
【００２３】
このように、請求項１の発明によれば、等価関係は、厳密な等価関係である必要はなく、所定の関係であれば足りるので、パラメータによる表示を含む論理型プログラムの比較による妥当性検証が可能になる。また、検証に適した規則性にしたがって構成された規範的なＦＳＭを得ることができるので、ＦＳＭ同士の比較が容易になる。
【００２４】
また、請求項２の発明では、汎化質問によって比較の対象となる変換内容が制限されるので、比較を効率的に行うことができる。
【００２５】
また、請求項３の発明では、変換ステップにおいて、各プログラムに静的解析を適用することにより、各データ型を容易に決定できるので、ユーザは、プログラムに基づいて各データ型を決定する煩雑な手数を省くことができる。
【００２６】
また、請求項４の発明では、比較ステップは、制約解法を用いて比較を行う。この制約解法においては、まず、入力、出力、または状態を表す各プログラム変数に固有の制約変数を割り当て、次に、第１の論理型プログラムから、特定のデータ型の各制約変数と、対応するデータ型の他の制約変数とがペアになるように制約変数をグループ化するとともに、第２の論理型プログラムから、特定のデータ型の各制約変数と、対応するデータ型の他の制約変数とをペアになるように制約変数をグループ化する。続いて、制約変数の各ペア間の非等価関係の連言（論理積）を生成するとともに、選言（論理和）形式の式について可能な全ての再配列に対して、個々の位置において生じる制約変数間に等価関係を生成し、さらに、生成された非等価関係の連言と等価関係を新たな式に対する制約として設定し、制約を用いてその新たな式を解く。したがって、請求項４の発明では、状態の内部表現が相違する有限状態機械同士を比較することができる。
【００２７】
また、請求項５の発明では、仕様言語によって多相性を直接表現できるので、従来の手法と比べて、より高度の抽象化が可能である。
【００２８】
また、請求項６の発明では、状態空間に存在するパターンを活用できるので、より多様な装置の比較が可能になり、また、比較全体の速度が向上する。
【００２９】
また、請求項７の発明では、遷移関数式を、共通値によって変数をグループ化するように並べ換え、固有コードによって符号化できるので、比較をより効率的に行うことができる。
【００３０】
【実施例】
次に、本発明による論理型プログラム検証方法を適用した実施例である論理型プログラム比較装置（以下「本装置」という）について、図面に従って具体的に説明する。
【００３１】
本装置はコンピュータ上に実現されるもので、本装置の各機能は、プログラムとして格納された所定の手順で前記コンピュータを動作させることによって実現されている。したがって、以下、本装置の各機能を有する仮想的回路ブロック（手段）を想定して本装置を説明する。
【００３２】
なお、前記コンピュータは、一般には、ＣＰＵ（中央演算処理装置）と、ＲＡＭ（随時書込読出型記憶素子）からなる主記憶装置とを有する。また、前記コンピュータの規模は自由であり、マイクロコンピュータ・パーソナルコンピュータ・スモールコンピュータ・ワークステーション・メインフレームなど、いかなる規模のものを用いてもよい。
【００３３】
また、前記コンピュータのハードウェアは、典型的には、キーボードやマウスなどの入力装置と、ハードディスク装置などの外部記憶装置と、ＣＲＴ表示装置やプリンタ印字装置などの出力装置と、必要な入出力制御回路を含む。
【００３４】
但し、前記コンピュータのハードウェア構成は自由であり、本発明が実施できる限り、上記の構成要素の一部を追加・変更・除外してもよい。例えば、本装置は、複数のコンピュータを接続したコンピュータネットワーク上に実現してもよい。また、ＣＰＵの種類は自由であり、ＣＰＵを複数同時に用いたり、単一のＣＰＵをタイムシェアリング（時分割）で使用し、複数の処理を同時平行的に行ってもよい。また、入力装置として、他の装置、例えば、タッチパネル・ライトペン・トラックボールなどのポインティングデバイスや、デジタイザ・イメージ読取装置やビデオカメラなどの画像入力装置・音声識別装置・各種センサを用いてもよい。また、外部記憶装置として、他の装置、例えば、フロッピーディスク装置・ＲＡＭカード装置・磁気テープ装置・光学ディスク装置・光磁気ディスク装置・バブルメモリ装置・フラッシュメモリなどを用いてもよい。また、出力装置として、他の装置、例えば、液晶表示装置・プラズマディスプレイ装置・ビデオプロジェクター・ＬＥＤ表示装置・音響発生回路・音声合成回路を用いてもよい。
【００３５】
また、前記コンピュータにおいて本装置を実現するためのソフトウェアの構成としては、典型的には、本装置の各機能を実現するためのアプリケーションプログラムが、ＯＳ（オペレーティングシステム）上で実行される態様が考えられる。また、本装置を実現するためのプログラムの態様としては、典型的には、高級言語やアセンブラからコンパイル（翻訳）された機械語が考えられる。但し、前記コンピュータのソフトウェア構成も自由であり、本発明が実施できる限り、ソフトウェア構成を変更してもよい。例えば、必ずしもＯＳを用いる必要はなく、また、プログラムの表現形式も自由であり、ＢＡＳＩＣのようなインタプリタ（逐次解釈実行型）言語を用いてもよい。
【００３６】
また、プログラムの格納態様も自由であり、ＲＯＭ（読出し専用メモリ）に格納しておいてもよく、また、ハードディスク装置のような外部記憶装置に格納しておき、コンピュータの起動時や処理の開始時に主メモリ上にロード（読み込み）してもよい。また、プログラムを複数の部分に分割して外部記憶装置に格納しておき、処理内容に応じて必要なモジュールのみを随時主メモリ上にロード（読み込み）してもよい。さらに、プログラムの部分ごとに異なった態様で格納してもよい。
【００３７】
なお、本明細書における各「手段」は、本装置の各機能に対応する概念的なもので、必ずしも特定のハードウェアやソフトウェア・ルーチンとの１対１対応関係を意味しない。例えば、同一のハードウェア要素が、場合によって異なった手段を構成する。また、一つの手段が、わずか１命令によって実現される場合もあれば、多数の命令によって実現される場合もある。
【００３８】
また、本実施例における各手順の各ステップは、その性質に反しない限り、実行順序を変更し、複数同時に実行し、また、実行ごとに異なった順序で実行してもよい。このような順序の変更は、例えば、ユーザが実行可能な処理を選択するなどメニュー形式のインタフェース手法によって実現することができる。
【００３９】
また、本明細書において「入力」というときは、本来の情報の入力のみならず、情報の入力と密接に関連する他の処理を含む。このような処理は、例えば、入力内容を確認のため出力装置へ出力（エコーバック）したり、入力内容の修正・編集である。また、本明細書における「出力」は、本来の情報の出力のみならず、情報の出力と密接に関連する他の処理を含む。このような処理は、例えば、出力すべき範囲の入力や、画面スクロールの指示である。なお、対話型インタフェースを用いて入力と出力を一体的操作によって実現してもよく、また、このような一体的操作によって「選択」、「指定」、「特定」など、何らかの出力情報に基づいた処理に適用し得る。
【００４０】
また、本明細書におけるデータ（情報）は、やデータの格納手段は前記コンピュータ上においていかなる態様で存在してもよい。例えば、データのハードウェア上の所在部分は、主記憶装置・外部記憶装置・ＣＰＵのレジスタやキャッシュメモリなどいかなる部分でもよい。また、データの保持態様も自由である。例えば、データは、ファイル形式で保持されるのみならず、メモリやディスクなどの記憶装置を物理的アドレスで直接アクセスすることによって実現してもよい。また、データの表現形式も自由である。例えば、文字列は、文字単位のコードで格納しても単語単位のコードで格納してもよい。また、データは必要とされる一定時間だけ保持されれば十分で、その後消滅してもよく、保持時間の長短は自由である。また、辞書データのように当面変更されない情報は、ＲＯＭに格納してもよい。
【００４１】
また、本明細書において、特定の情報への言及は確認的で、言及されない情報の存在を否定するものではない。すなわち、本発明の動作では、動作に必要な一般的な情報、例えば、各種ポインタ、カウンタ、フラグ、パラメータ、バッファなどが適宜用いられる。
【００４２】
本装置の各部分が処理に要する情報は、特に記載がない場合、当該情報を保持している他の部分から獲得される。このような情報の獲得は、例えば、当該情報を格納している変数やメモリをアクセスすることによって実現することができる。なお、情報の消去・抹消は、当該情報の内容自体を必ずしも記憶領域から現実に削除せず、消去を表すフラグを設定するなど、情報の意味付けの変更によって行うことができる。
【００４３】
また、本装置はコンピュータ上に実現されているが、本装置の機能の全部又は一部は専用の電子回路上に実現してもよい。
【００４４】
１．実施例の構成…図１
本装置は、図１（本装置のブロック図）に示すように、キーボード１と、表示装置２と、Ｉ／Ｏ制御回路３と、キーボード１を通じての論理型プログラムの入力動作を制御する入力部４とを有する。また、本装置は、各論理型プログラムをＦＳＭに変換する変換部５（前記変換手段に相当するもの）と、２つのＦＳＭを比較する比較部６（前記比較手段に相当するもの）と、表示装置２を通じての前記比較結果の出力動作を制御する出力部７とを有する。なお、キーボード１、Ｉ／Ｏ制御回路３及び入力部４は前記入力手段を構成し、出力部７、Ｉ／Ｏ制御回路３及び表示装置２は前記出力手段を構成している。
【００４５】
２．実施例の作用…図２〜図１７
上記のような構成を有する本装置における論理型プログラムの比較は、次のように行われる。
【００４６】
２−１．論理型プログラムの入力
まず、ユーザは、キーボード１から、システムの仕様及び実システムの内容を、論理型プログラムの形式で本装置に入力する。なお、論理型プログラムは、一般に、論理プログラミング言語によって記述され、この論理プログラミング言語は、述語論理などの論理言語体系に基づいて構成される。本実施例における論理プログラミング言語は、次のような述語論理を基礎とするものである。
【００４７】
２−１−１．述語論理
すなわち、ここでいう述語論理は、項の全体集合によって定義されるものである。例えば、全体集合における項ｔは、変数Ｖともなり得るし、また、０に関する（０項の、即ち項目の数が０個の）関数記号ｆ（以下、「定数」という。）ともなり得るし、さらに、再帰的に構成される項“ｆ（ｔ１，・・・，ｔｎ）”（但しｎ＞０）ともなり得る。この場合、ｆはｎに関する（ｎ項の、即ち項目の数がｎ個の）関数記号であり、ｔ１，・・・，ｔｎは全体集合に含まれている項である。
【００４８】
なお、このような項は、語義どおりの存在を意味するのに用いられる。例えば、定数“０”は、整数のゼロの意味に用いることができる。また、二分岐関数記号“ｎｏｄｅ”は、二分岐ツリーにおいて、左に分岐すればｔ１、右に分岐すればｔ２に到達するような、ノード（ｔ１，ｔ２）を意味するのに用いることができる。
【００４９】
このような項の全体集合において要素間の関係を表すには、原子論理式を用いる。すなわち、一つの原子論理式はｎに関する述語記号ｐであり、ｎ個の引数をとる。但し、ｎ＝０の場合、その原子論理式は命題と呼ばれ、単に“ｐ”のように記述される。ｎ＝０でない場合、原子論理式は、ｔ１，・・・，ｔ２を項とすれば、“ｐ（ｔ１，・・・，ｔ２）”のように記述される。また、述語論理では、原子論理式Ａ、又は、原子論理式Ａの否定
【数１】
0003582849.tif 000002
のいずれともなり得るものとして、リテラルが定義される。
【００５０】
なお、述語論理における論理式は、次のような接続子を用いて構成される。
【数２】
0003582849.tif 000003
ここで、上記接続子は、左から順にそれぞれ、否定、連言、選言、含意、限定、一般的量化を表す。例えば、Ａがリテラル、Ｖが変数、Ｆ１及びＦ２が論理式とした場合、次のようなものも論理式となる。
【数３】
0003582849.tif 000004
また、論理式のうち、一定の、そして通常は単純な書式が「節」と呼ばれる。述語論理で用いられるセンテンス（一連の文）は、このような節の集合として定義され、これら節の結合として解釈される。
【００５１】
２−１−２．論理プログラミング言語
本実施例における論理プログラミング言語は、プロログ（Ｐｒｏｌｏｇ）の変形であり、上記のような論理言語の部分集合である。すなわち、この部分集合は、上記述語論理のうち、この部分集合によって記述されるような問題について、効率的な解決手順が存在するものである。このような述語論理の部分集合は、「確定節」として知られており、確定節は、次の３つの書式の一つに限定された論理式である。
【数４】
0003582849.tif 000005
ここで、Ｈは原子論理式、Ｂは（空でない）リテラルの連言、□は真の述語（すなわち、恒真である関係）、Ｖ１，・・・，Ｖｎは、ＨやＢにおいて生じる変数である。上記数式４における第１の書式は「質問」と呼ばれ、第２の書式は「ルール」と呼ばれ、第３の書式３は「事実」と称されている。
【００５２】
本実施例における論理型プログラムは、上記のような確定節の集合によって構成されたセンテンスである。そして、論理型プログラムでは、上記の「質問」がそのプログラムによって解決されるべき課題を表す。このような課題は、例えば、
【数５】
0003582849.tif 000006
が偽であることの証明によって構成される。この例における証明は、すなわち、「Ｂが真」というような変数Ｂへの代入の存在の証明を意味する。
【００５３】
以下の説明では、上記の論理プログラミング言語を前提とし、プロログ文法に近い表記法によって論理型プログラムを表す。すなわち、連言接続子はカンマと共に（カンマを使用して）記述し、選言及び一般的量化の記号は省略し、節の終りはピリオドで表す。また、変数名は大文字から開始し、述語記号及び関数記号は小文字又は数字から開始する。さらに、リストに関する便宜的表記法として、
【数６】
［］
は空のリストを、［ｔ１｜ｔ２］は、最初の要素が項ｔ１、最後の要素が項ｔ２であるようなリストを表し、また、［ｔ１，・・・，ｔｎ］は項のリストｔ１，・・・，ｔ２を表す。
【００５４】
ここで、上記「質問」と、スタックの操作を定義する単純な論理型プログラムの一例を図２に示す。この図では、１行目が「質問」になっており、２行目から５行目は述語記号“ｓｔａｃｋ”によって表される関係を定義している。この定義は再帰的であり、引数１から５で与えられた複数の値のリストについて、各リストが全て終了するまで所定の操作を繰り返す動作を表している。なお、各リストにおける繰り返しは、ハードウェア・クロックの１サイクルを表し、また、述語記号“ｓｔａｃｋ”の６つ目の引数は値のスタックを表す。
【００５５】
また、図２において、６〜９行目は、述語記号“ｓｔａｃｋＢｏｄｙ”を定義する「事実」であり、述語記号“ｓｔａｃｋ”の最初の５つの引数は、スタックに転送され又はスタックから転送される一連の値を示すのに用いられるリストである。そして、述語記号“ｓｔａｃｋＢｏｄｙ”によって表現される関係は、スタック操作を表している。また、定数“ｎｏｐ”はアイドリング・サイクルを意味し、“ｅｘｅｃ”は実行サイクルを意味する。さらに、定数“ｐｕｓｈ”及び“ｐｏｐ”は、それぞれ、スタックへの要素の積み上げ（プッシュ）又はスタックからの要素の取り出し（ポップ）を起動する命令を表している。
【００５６】
また、定数“ｏｋ”及び“ｅｒｒｏｒ”は操作が有効であったか無効であったかを知らせる信号として用いられる。さらに、述語記号“ｓｔａｃｋＢｏｄｙ”の３番目の引数は、プッシュ操作（７行目）においてスタックにプッシュされる要素を意味し、４番目の引数は、正常なポップ操作（８行目）においてスタックからポップされる要素を意味する。また、６番目の引数は操作前のスタックを意味し、７番目の引数は操作実行の結果であるスタックを意味する。
【００５７】
このような論理型プログラムの「質問」（１行目）は、当該論理型プログラムが解決しようとする問題の論述を表し、具体的には、当該質問における原子論理式が真になるような出力信号“Ｏ”及びエラー信号“Ｅ”の値を決定することを意味している。この例では、質問に対して無数の解の候補が存在する。すなわち、ｔ１，ｔ２及びｔ３が任意の項とした場合、“Ｏ”は値［ｔ１，ｔ２，ａ，ｔ３］を取ることができ、また、“Ｅ”は値［ｏｋ，ｏｋ，ｏｋ，ｅｒｒｏｒ］を取ることができる。
【００５８】
２−１−３．質問の解決
なお、このような質問の解は、接続子“←”の右辺の原子論理式を手続呼出と考えることで得ることができる。この場合、接続子“←”の左辺に位置し、前記手続呼出と同じ述語記号及び（多ソート代数にいう）アリティを有する節の集合が手続定義に相当する。このような質問の解決では、最初の質問Ｑから、原子論理式Ａ（但しＡ≠□）が選択されて除去され、Ｑ´が残る。その後、手続呼出とみなされる原子論理式Ａは、対応するものが発見されるまで、手続の連言の節における左辺の原子論理式と比較される。この比較において、２つの原子論理式は、両原子論理式中の変数について、両者が等しくなるような置換候補が存在するとき、適合するとされる。このような適合対象を求める手続をマッチングという。
【００５９】
例えば、変数の置換候補の集合θによってＡ１がＡに適合するような節“Ａ１←Ｂ”を仮定した場合、
【数７】
0003582849.tif 000007
に置換候補θを適用した結果が新たな「質問」として扱われ、この質問に上記のようなマッチング処理が再帰的に適用されれば、質問Ｑを解決することができる。この処理は、上記のように新たに発生した中間的質問が、□のみによって構成された状態に到達したときに終了する。質問に対する解は、最初の質問Ｑに、上記のような全ての置換候補を適用することによって導かれる。
【００６０】
なお、上記のように発生する中間的質問の解決中に、選択されたある質問に適合する節が存在せず、解決に「行き詰まった」場合、バックトラッキング（後戻り）が開始される。バックトラッキングによれば、「質問」の解決のために、上記のような「適合」の条件を満たす他の節を探索することができる。なお、この場合、他の節の探索に先立って、上記のような行き詰まりに至るまでに生成された変数の置換候補は、全て消去される。
【００６１】
論理型プログラムにおいては、上記のように、最初の質問が、特定の質問に対する論理型プログラム解決システムの答えを求めることを意味している（例えば、図２における質問は、出力信号Ｏ及びエラー信号Ｅについて、質問の記述内容を満たすような値を要求している。）。そして、本実施例における検証手続の目的は、２つの論理型プログラム（すなわち仕様及び実システム）が、あり得る全ての質問に対して同一の動作を提供するか否かを決定することである。
【００６２】
ここで、論理プログラムとしては多様な質問がありうるが、仕様記述として意味があるのはその一部である。例えば、図２に示したようなハードウェアスタックの記述について、たとえば、出力値およびエラー信号を与えて、入力信号や制御、モードを逆算するようなことは論理型プログラムとしては計算可能だが、仕様記述としては必要はない。
【００６３】
本実施例の仕様言語によれば、多相性を直接表現できるので、従来の手法と比べて、より高度の抽象が可能である。
【００６４】
２−１−４．汎化質問
そして、このように現実の動作において考えられる、より少ない質問の集合についてのみ２つの論理型プログラムを比較すれば、検証所要時間は大幅に短縮することができる。そこで、このような少ない質問の集合を、「汎化質問」という概念によって表現することとする。この汎化質問は、プログラムの一部として入力され、環境宣言部及びインタフェースという２つの部分から構成される。このうち、インタフェースは、検証対象となる構成要素における対外入出力ポートを定義する。この場合、妥当性の検証は、インタフェースに現れる振る舞いに関して行われ、当該構成要素における内部構造の詳細は重要でないものとして無視することができる。また、環境宣言部は、検証対象となる構成要素において、通常の動作において現れ得る入力値の集合を特定する役割を果たす。
【００６５】
図３は、汎化質問（１行目）を、環境定義の補助に必要ないくつかの追加的な節と共に示している。最初の４つのアトム（記述単位）は、汎化質問の環境宣言部を構成している。これらのアトムは、プログラム実行中にスタックへの入力が持ち得る値のデータ型を定義している。また、汎化質問の５番目のアトムは、インタフェースを定義しており、この例におけるインタフェースは、スタックへのインタフェースによって構成されている。
【００６６】
２−２．論理型プログラムのＦＳＭへの変換
２−２−１．静的解析によるデータ型の獲得
入力された論理型プログラムは変換部５に転送され、静的解析によって、論理型プログラム実行中における変数のデータ型が決定される（参考文献：Ｍａｕｒｉｃｅ  Ｂｒｕｙｎｏｏｇｈｅ  ａｎｄ  Ｇｅｒｄａ  Ｊａｎｓｓｅｎｓ．  Ａｎ  ｉｎｓｔａｎｃｅ  ｏｆ  ａｂｓｔｒａｃｔ  ｉｎｔｅｒｐｒｅｔａｔｉｏｎ  ｉｎｔｅｇｒａｔｉｎｇ  ｔｙｐｅ  ａｎｄ  ｍｏｄｅ  ｉｎｆｅｒｅｎｃｉｎｇ．  Ｉｎ  Ｔｈｅ  ＭＩＴ  Ｐｒｅｓｓ，  ｅｄｉｔｏｒ，  Ｌｏｇｉｃ  Ｐｒｏｇｒａｍｍｉｎｇ：  Ｆｉｆｔｈ  Ｉｎｔｅｒｎａｔｉｏｎａｌ  Ｃｏｎｆｅｒｅｎｃｅ  ａｎｄ  Ｓｙｍｐｏｓｉｕｍ，  ｐｐ．  ６６９−６８３．  ＩＥＥＥ，  Ａｕｇｕｓｔ  １９８８．）。すなわち、静的解析によれば、各種最適化に有用な情報を提供できるので、本実施例では、ユーザに必要な情報を問い合わせることなく、静的解析を用いている。
【００６７】
ここで、論理型プログラムにおいて、データ型は、論理型プログラムで用いられる変数がプログラム実行中に値として取り得る項の集合を表現したものである。すなわち、データ型は、“τ→｛ｕ１，・・・，ｕｎ｝”のような書式規則の集合によって定義される。ここで、τはデータ型を意味するデータ型変数であり、ｕ１，・・・，ｕｎはデータ型の項である。データ型の項は、原則的には通常の論理項と同様に構成されるが、変数としては、通常の論理変数の代りにデータ型変数が用いられる。また、あり得る全ての項を表す特殊なデータ型は“Φ”と表され、この場合、どのデータ型τについても次の関係が成立する。
【００６８】
【数８】
0003582849.tif 000008
【００６９】
図３に示す汎化質問に静的解析を適用すると、その結果として図４に示すようなデータ型規則集合が得られる。また、実行中の変数のデータ型は図５及び６に示すような内容となる。このうち図５は手続の入口（エントリ）におけるデータ型であり、図６は手続の出口におけるデータ型である。なお、汎化質問の環境宣言部におけるこれら呼出の型は、静的解析に続く以下の手順においては無視され、参照されることはない。これらの解析結果は、論理型プログラムのＦＳＭへの変換において用いられる。
【００７０】
２−２−２．ＦＳＭ
続いて、各論理型プログラムは、比較のために（比較の基準となる）規範的ＦＳＭに変換される。ここで、図７は、ＦＳＭの基礎となる有限状態機械の全体構成を示す概念図であり、入力ポートＩ、出力ポートＯ、遷移関数ｆ及び状態レジスタＲを示している。すなわち、ＦＳＭでは、遷移関数ｆが、現在の状態Ｓ及び現在における入力ポートＩからの入力を取得し、出力ポートＯからの出力及び次の状態ＮＳを演算する。そして、状態レジスタＲは、現在のサイクル実行中は次の状態ＮＳを格納し、この次の状態ＮＳは次のサイクルにおける状態として用いられる。
【００７１】
上記のような次状態への遷移関数を規範的表現において用いることによって、２つのＦＳＭの比較における問題が単純化なものとなる。すなわち、ｆｓ及びｆｉをそれぞれ仕様及び実システムに対応する遷移関数とし、ｆｓ及びｆｉが共に規範的（ＦＳＭ）形式で表されているとする。このとき、あり得る全ての入力Ｉ及び現在の状態Ｓに対してｆｓ（Ｉ，Ｓ）＝ｆｉ（Ｉ，Ｓ）ならば、ｆｓの規範的形式はｆｉの規範的形式と同一と考えることができる。
【００７２】
論理型プログラムをこのような規範的ＦＳＭ形式に変換するには、論理型プログラムの表記法に内在する構造を除去するため、いくつかのステップが必要である。最初のステップでは、論理型プログラムにおける「節」という構造の一部を除去するため、手続を定義する複数の節を、完備形式として知られる単一の節に合成する。ここで、ｎ項のある述語記号ｐに関する手続定義がｍ個の節：
【数９】
0003582849.tif 000009
から構成されている場合、ｐの完備形式を構成するには、まず、新たな変数Ｖｉ（但しｉ＝１・・・ｎ）が生成される。これらの変数と項ｔｊｉ（但しｉ＝１・・・ｎ，ｊ＝１・・・ｍ）を用いて、新たな原理論理式Ｖｉ＝ｔｊｉが各ｉ＝１・・・ｎ，ｊ＝１・・・ｍについて生成される。なお、ここで、ｔｊｉは前記ｍ個の節のｎパラメータであり、また、“＝”は等価関係を表す項で、「ｔ１とｔ２が一致するとき、およびそのときにかぎり原子論理式“ｔ１＝ｔ２”は真である。」ということを表す。前記の各節のうち、これらの原子論理式とボディＢｊ（但しｊ＝１・・ｍ）を用いて、ｐの完備形式が次のような形式となる。
【数１０】
0003582849.tif 000010
この手順は、全ての手続定義が完備形式となるまで繰り返される。図８は、図２のスタックプログラムに基づいた完備形式である。
【００７３】
２−２−３．手続呼出階層の平坦化
次のステップは、手続呼出階層の平坦化によって構成され、このステップによって、呼出は手続ボディによって置き換えられる。この置換えは、「展開」として知られ、この展開では、手続ボディ内の変数は呼出引数によって置き換えられ、また、手続に対してローカルな変数に対しては、識別性が保たれるように適当な名称変更が施される。
【００７４】
平坦化手続においては、再帰的呼出の処理が一つの問題となる。すなわち、再帰的手続は、実行中、呼出結果を最終的にその再帰的手続自体に戻すような呼出を含む手続である。例えば、図２の手続“ｓｔａｃｋ”はその５行目に呼出を有しているが、この呼出は、この呼出自身が含まれている手続自体に対する（直接の）再帰的呼出である。
【００７５】
呼出を非再帰的手続に展開し続けると、プログラムは最終的に、非再帰的手続への呼出がもはや残らないものになる。そして、再帰的手続呼出の処理に際して、どの再帰的呼出を手続ボディによって連続的に展開した場合に、処理終結が導かれるかを決定するには、次のような手法が用いられる（参考文献：Ｍ．Ｂｒｕｙｎｏｏｇｈｅ  ｅｔ  Ｄａｎｎｙ  Ｄｅ  Ｓｃｈｒｅｙｅ  ａｎｄ  Ｂｅｒｎ  Ｍａｒｔｅｎｓ．  Ａ  ｇｅｎｅｒａｌ  ｃｒｉｔｅｒｉｏｎ  ｆｏｒ  ａｖｏｉｄｉｎｇ  ｉｎｆｉｎｉｔｅ  ｕｎｆｏｌｄｉｎｇ  ｄｕｒｉｎｇ  ｐａｒｔｉａｌ  ｅｖａｌｕａｔｉｏｎ．  Ｎｅｗ  Ｇｅｎｅｒａｔｉｏｎ  Ｃｏｍｐｕｔｉｎｇ，  ｐｐ．  ４７−７９，  Ｎｏｖｅｍｂｅｒ  １９９２．）。すなわち、ここでは、どの再帰的呼出が数量的にある程度“小さい”二次的再帰的呼出を常に生じるかが検出され、それによって、最終的には、サイズがゼロの呼出、換言すれば、再帰的手続への他の呼出を生じない呼出を、結果的に得ることができる。
【００７６】
ところで、図９は、スタックプログラムの他の一例であり、ここでは、スタックにプッシュされ得る要素の数が３つに制限されている。期待される実行モードでは、関係“ｌｅｎ”は、最初の引数で与えられたリストの長さを算出し、それを２番目の引数に戻すことを意味している。ここでは、挿入辞的に（インフィックス記法／中置表記法で）表記される“＜”や“ｉｓ”が意味する関係は、システムに組み込みのものと想定する。なお、“＜”が意味する関係は、２つの引数が整数であり、かつ、最初のものが２番目のものよりも厳密な意味で小さいときに真となる関係である。また、期待される実行モードでは、関係“ｉｓ”はその右側の式の値を求め、その結果を述語記号“ｉｓ”の左側の変数に代入するものとして働く。
【００７７】
そして、図１０は、図９の（スタックに要素が３つ入っている）スタックプログラムの完備形式を示しており、図１１は、当該プログラムの平坦化されたものである。なお、再帰的手続“ｌｅｎ”に対する呼出は拡張されているが、これは、その２番目の引数が、常に３という上限を有するからである。
【００７８】
２−２−４．ＦＳＭへのマッピング
以上のように平坦化された後のプログラムには、再帰的手続の呼出のみが残ることとなる。再帰的手続のマッピングは、再帰的手続の手続ボディを、次のような反復的表現に対する再帰的呼出を除いてＦＳＭにマッピングすることによって行われる。
【数１１】
0003582849.tif 000011
ここで、Ｒは状態レジスタ、関数ｌ及びｒはそれぞれ、一組の引数の左側及び右側の要素を返す関数である。数式１１に示したような繰り返し形式（ｆｓｍ）は、次のような初期状態に加え、一連の入力値から一連の出力値を生成する再帰的手続と等価である。
【００７９】
【数１２】
0003582849.tif 000012
ここで、遷移関数は述語表記で書かれ、左右選択関数ｌ及びｒはマッチングを通じて実現されている。
【００８０】
ところで、ＦＳＭの述語表記では、入力リスト及び出力リストは、遅延評価と同様の手法で一時的な変数領域で処理される変数の順序を示す。このため、リスト全体を格納するためにメモリを要することはない。しかし、前記ｆｓｍの３番目の引数は、入力リスト及び出力リストにおけるリストの位置が前進したり、現在状態Ｒｉが次の状態Ｒｉ＋１  によって上書きされるときにおける空回り状態を回避するために、ストレージ・レジスタを包含する（表している）。
【００８１】
平坦化されたプログラムにおける再帰的呼出は、上記手続ｆｓｍと構造が同一のパターンを発見するために解析される。すなわち、再帰的呼出のエントリ型（入口の型）及び出口型（出口の型）の解析によって、つまり、呼出しの入口点と出口点の型を解析することで、どの引数が、一時的変数領域で処理され得る列型を意味するかが決定される。この列型は次のような書式となる。
【数１３】
0003582849.tif 000013
ここで、τは列型を意味するいずれかの型変数、τｅはリストの要素型を意味する型変数、ｆ０は任意の定数、ｆ１は任意の２引数の関数記号である。例えば、リスト表記
【数１４】
0003582849.tif 000014
はしばしば列型として用いられる。
【００８２】
再帰的手続の引数はさらに入力リストと出力リストとに区分される。ここで、呼出の引数のエントリ型（例えば図５）がΦ型を含まない列型（すなわち基底型）の場合、引数は入力リストである。エントリ型が、Φ型と等しい場合も、要素型τｅがΦ型である列型と等しい場合も、引数は出力リストである。また、入力リスト又は出力リストのいずれでもない引数は、状態レジスタに区分される。そして、１つ以上の入力リスト及び１つ以上の出力リストを有する再帰的手続は、上記再帰的手続ｆｓｍで説明したようなＦＳＭ形式に直接対応する。
【００８３】
なお、本実施例では、論理型プログラムをＦＳＭ形式に変換するプロセスが必要なため、いくつかの制限が存在する。すなわち、ｆｓｍで説明したＦＳＭ形式にマッピングできないような再帰的手続を含むプログラムは、取り扱うことができない。また、機械は有限状態でなければならず、さらに、状態の表現は有限でなければならないため、さらなる制約が状態レジスタの表現に適用される。なお、任意の論理型プログラムを比較する場合の問題は予測不能であるため、その内容に応じていくつかの制約が生じ得る。
【００８４】
上記のような制約を満たす論理型プログラムは、１以上のＦＳＭの連携から構成される。因みに、図１０の完備形式は、ｆｓｍで説明した書式に直接マップされるので、このような制約を満足することとなる。また、小さなＦＳＭの連鎖によって構成されるプログラムでは、小さなＦＳＭの状態表現の全てを連鎖させることによって全体の状態表現を構成し、大きな単一のＦＳＭが構築することができる。このような場合、全体としての遷移関数も、小さなＦＳＭの遷移関数の連鎖として構成される。以上の結果、入力リスト引数（すなわちＩ）、出力リスト引数（すなわちＯ）及び単一の状態レジスタ引数（すなわちＲ）を有する単一の再帰節が得られる。
【００８５】
遷移関数は、このような単一の再帰節から導かれた“Ｈ←Ｂ”という形式の新たな手続である。この遷移関数のボディＢは、単一の再帰節のボディから、リスト関連処理と同様に再帰的呼出を除去した結果得られる表現である。Ｈの引数は、再帰節の列型から状態及び次状態変数と組み合わせて抽出された個々の入出力要素である。すなわち、Ｈの引数は、列型から選択された入出力要素に対応するものと、状態及び次状態変数と、を含む。
【００８６】
なお、入出力の引数における位置は、要素選択の対象となるリスト上の位置に対応するように、注意深く整えられる。すなわち、状態及び次状態の引数は、常に、遷移関数の最後から２つの引数位置に配置される。完備形式は、遷移関数を表す手続が、原子論理式中において接続子“←”の左側にのみ変数を有することが確実となるように適用される。
【００８７】
なお、図１２は、図１０から抽出された遷移関数を示す図である。ここでは、関数が仕様ＦＳＭの遷移関数であることを表示するのに、述語記号“ｓｐｅｃ”が用いられている。
【００８８】
２−２−５．ボディの並べ換え
そして、次のような手順によって遷移関数のボディを並べ変えると、規範に近い決定木と呼ばれる記述が得られる。
【００８９】
２−２−５−１．Ｖが入力、出力又は次の状態変数とした場合、各原子論理式“ｔ＝Ｖ”を原子論理式“Ｖ＝ｔ”に並べ変える。
【００９０】
２−２−５−２．Ｖ１は連言において以外に生じず、また、Ｖｉｎを入力変数とした場合、“Ｖｉｎ＝Ｖ１”のような形式の原子論理式を除去する。このステップによって、無意味な比較を回避することができる。
【００９１】
２−２−５−３．原子論理式を比較と代入とに区分する。ここで、比較は、Ｖｉｎが入力変数又は現在状態変数で、ｔが任意の項の場合において、“Ｖｉｎ＝ｔ”という形式の原子論理式である。また、代入は、Ｖのエントリ型がΦの場合において、“Ｖ＝ｔ”という形式の原子論理式である。
【００９２】
２−２−５−４．変数Ｖ１，Ｖ２，・・・，Ｖｌ−１を、遷移関数への引数として現れる順序の入力変数とし、また、Ｖｌを現在状態変数とする。また、｛Ｖｉ＝ｔｉ１，・・・，Ｖｉ＝ｔｉｎ｝をＶｉにおける一般的な比較の集合とする。このとき、遷移関数の手続ボディは、図１３に示すような形式に再構築される。この図１３において、ノードは入力及び状態変数Ｖｉ（但しｉ＝１・・ｌ）を表し、項ｔｉ１，・・・，ｔｉｎがラベルとなっているノードＶｉからのエッジは、選言の接続子Ｖ（ＯＲ）で接続されているように、二者択一の比較Ｖｉ＝ｔｉｊ（但しｊ＝１・・ｎ）を表している。このツリーにおける（いわば）葉は、出力変数への代入が順列し及び冒頭に配置されるように配置換えされた入力及び状態変数、との比較を必要としない表現である。この表現には、次状態変数に値を代入する表現が続く。
【００９３】
なお、前記変数の順序Ｖ１，Ｖ２，・・・，Ｖｌ−１は、一定で、この変数順序によれば、前記比較の集合｛Ｖｉ＝ｔｉ１，・・・，Ｖｉ＝ｔｉｎ｝を並べ換えることによって、表現は規範的表現に近いものとなる。なぜならば、いかなる等価な有限状態機械も、同一の入力を与えられた場合、同様な順序の比較を有するからである。図１４は、このようにボディを決定木に並べ換えた後の遷移関数を示す図である。
【００９４】
なお、ここで、Ｖｓを現在状態変数とした場合、ｔが状態型における複数の項に適合する場合における“Ｖｓ＝ｔ”という形式の比較は、節の平坦化に類似した処理を用いることによって平坦化され、遷移関数で生じる全ての項が独特の項を生じることとなる。図１５は、このようなスタック状態の平坦化の結果を示す図である。
【００９５】
２−２−６．状態の符号化
さらに、ＦＳＭの状態の検出は、まず、遷移関数中で生じる状態の各項ｔをペアｉ：＜Ｖ１，・・・，Ｖｎ＞に変換することによって実現される。なお、ここで、ｉは固有の整数であり、＜Ｖ１，・・・，Ｖｎ＞は、多相変数のベクトルである。この場合、変数Ｖ１，・・・，Ｖｎを含み、これら各変数がそれぞれエントリ型及び出口型Φを有する項ｔについては、変数Ｖ１，・・・，ＶｎはＦＳＭの多相パラメータを表す。また、ベクトル＜Ｖ１，・・・，Ｖｎ＞は、ｔの変数のリストによって構築され、このリストによる構築は、あらかじめ定められた順列規則（典型的には深さ優先で、左から右向きの順列）にしたがって行われる。これらベクトルは、全てのベクトルが等しい長さになるように、固有の変数と共に右詰めで配置される。整数ｉのペアに代入される内容は、多相変数の改名によって、状態型の項を検出し、各項に固有の整数を代入することによって決定される。なお、図１６は前記スタックの例における遷移関数の最終的な規範的形式を示す。
【００９６】
なお、以上のような変換に失敗した場合は失敗がユーザに報知される。
【００９７】
２−３．ＦＳＭの比較
以上のように変換された第１及び第２のＦＳＭは比較部６に転送され、比較部６が両ＦＳＭの等価性を検証する。２つのＦＳＭが等価であることを検証するには、まず、各機械の入力、出力及び状態の表現を符号化したものの間で、各遷移関数が等しいという等価関係が確認されなければならない。
【００９８】
まず、ここで、Ｅｉ，Ｅｏ及びＥｓを、それぞれ、両機械間における入力、出力及び状態の表現の等価関係とする。この場合、例えば、等価関係Ｅｉは、ペア（ｔ１，ｔ２）の集合であり、この場合におけるｔ１は、第１のＦＳＭにおける入力型の要素たる項である。また、ｔ２は、第２のＦＳＭにおける入力型の要素たる項である。等価関係Ｅｏ及びＥｓにおいても同様である。
【００９９】
本実施例において、等価関係Ｅｉ及びＥｏはいずれも、実行時間短縮のためユーザが入力してもよいし、また、等価関係Ｅｓと共に算出されてもよい。
【０１００】
そして、ｆ１及びｆ２を、ぞれぞれ、第１のＦＳＭ及び第２のＦＳＭにおける遷移関数とし、ｆ´２を、ｆ２の各入力、出力及び状態の項をそれぞれ、Ｅｉ、Ｅｏ及びＥｓに含まれるペアの該当要素で置き換えた関数とすると、２つの有限状態機械はｆ１＝ｆ´２のとき等価である。
【０１０１】
２−３−１．制約解決器
このようなｆ１＝ｆ´２を満足するような等価関係Ｅｉ、Ｅｏ及びＥｓを求めるには、制約解決器が用いられる。ここで、制約とは、型のとり得る値に対してその部分集合を規定する条件である。そして、この場合の制約は、非等価関係の連言のみならず、制約変数における等価関係の連言の選言から構成される。
【０１０２】
ここでは、具体的には、各ＦＳＭにおける各入力、出力及び状態の項に対して、固有の制約変数が生成される。なお、非等価関係は、ある一つの機械において、２つの等しい入力項の不存在、２つの等しい出力項の不存在、及び、等しい２つの状態値の不存在を、条件として指定する。これは、次のように表される。
【数１５】
0003582849.tif 000015
ここで、各ｉ１ｊ（但しｊ＝０・・ｐ）、ｏ１ｋ（但しｋ＝０・・・ｑ）及びｓ１ｌ（但しｌ＝０・・ｒ）は、第１のＦＳＭに基づいた制約変数であり、それぞれ、入力型、出力型及び状態型を表している。同様のルールは、ＦＳＭ２のｉ２ｊ、ｏ２ｋ、ｓ２ｌについても生成される。
【０１０３】
残る等価関係の連言の選言（すなわち積の合計（和））は、全ての可能なｆ１の再配列ｆ１１，ｆ１２，・・・，ｆ１ｎを得ることによって生成される。このようなｆ１の再配列は、選言における表現を変換することによって得られる。すなわち、
【数１６】
0003582849.tif 000016
は、
【数１７】
0003582849.tif 000017
と変換される。
【０１０４】
ここで、各ペアｆ１ｉ及びｆ２は同時に検討され、それによって、両者が構造的に同一か（すなわち、両者の決定木が構造的に同一か）否かが決定される。両者が構造的に同一の場合、連言が等価“Ｖ１＝Ｖ２”の間に配列される。ここで、Ｖ１は項ｔ１の制約変数、Ｖ２はｔ２の制約変数であり、また、ｔ１は第１のＦＳＭの一つの入力（、出力、状態）項であって、前記検討中に第２のＦＳＭの項ｔ２に適合したものである。選言は、構造的に同一のペアの各連言に基づいて形成される。
【０１０５】
このように生成された制約に基づいて第１及び第２のＦＳＭの間における等価性が判定され、その判定結果が出力部７を通じ、表示装置２に表示される。なお、図１７は、以上の論理型プログラム比較手順の大まかな流れを示すフローチャートである。
【０１０６】
３．実施例の効果
以上のように、本実施例によれば、比較の基礎となる等価関係は、厳密な等価関係である必要はなく、所定の関係であれば足りるので、パラメータによる表示を含む論理型プログラムの比較による妥当性検証が可能になる。また、本実施例では、検証に適した規則性にしたがって構成された規範的なＦＳＭを得ることができるので、ＦＳＭ同士の比較が容易になる。また、本実施例では、汎化質問によって比較内容が制限されるので、比較を効率的に行うことができる。また、本実施例では、変換部５が、各プログラムに静的解析を適用することによって前記データ型を獲得するので、ユーザは、プログラムに基づいてデータ型を決定する煩雑な手数を省くことができる。
【０１０７】
また、本実施例では、比較部６が、制約解決器を用いて前記比較を行うので、状態の内部表現が相違する有限状態機械同士を比較することができる。このため、本実施例によれば、ユーザは、比較対象となる各有限状態機械の各状態表現から対応関係を発見する煩雑な手順から解放される。さらに、本実施例は、パラメトリック多相変数を用いて表現された状態を有する有限状態機械（すなわち、パラメトリックに（パラメータを用いて）表現された状態を含む有限状態機械）同士の比較が可能になるという利点を有する。
【０１０８】
また、本実施例では、状態空間に存在するパターンを活用できるので、より多様な装置の比較が可能になり、また、比較全体の速度が向上する。また、本実施例では、多相性が、汎化された機械を比較できる有力な機構を提供したが、これは、多相性の各事例（要素）を、状態空間における単一のパターンとして取り扱うことによって実現されたものである。
【０１０９】
４．他の実施例
なお、本発明は上記実施例に限定されるものではなく、次のような他の実施例をも包含するものである。例えば、上記実施例では、データ型に関する情報は静的解析によって得られるが、このような情報は、他の解析手法や手入力など静的解析以外の手段によって獲得してもよい。また、汎化質問に示される情報についても手入力によって獲得するか、又はなんらかの解析手法によって獲得するかは自由である。
【０１１０】
【発明の効果】
以上のように、本発明によれば、パラメータによる表示を含む論理型プログラムについても比較による妥当性検証が可能で、しかも、このような検証を効率的に実現する、優れた論理型プログラム検証方法を提供することができる。
【図面の簡単な説明】
【図１】本発明の実施例の論理型プログラム比較装置のブロック図。
【図２】本発明の実施例における、スタック操作を表す論理型プログラムの一例の内容を示す図。
【図３】同実施例における汎化質問の内容を示す図。
【図４】図３に示した操作環境において、図２に示したプログラムに由来する型規則の集合を示す図。
【図５】図２のプログラムに基づく、手続呼出エントリにおける変数型の内容を示す図。
【図６】図２のプログラムに基づく、手続呼出出口における変数型の内容を示す図。
【図７】有限状態機械の要部のブロックダイヤグラム。
【図８】図２のプログラムの各節に基づいた完備形式の内容を示す図。
【図９】本発明の実施例におけるスタック操作プログラムの他の一例であって、スタックの深さが３に制限されているもの。
【図１０】図９に示した各節に基づいた完備形式の内容を示す図。
【図１１】図１０の完備形式に平坦化を施した結果の内容を示す図。
【図１２】図１１の平坦化されたプログラムから抽出された遷移関数の内容を示す図。
【図１３】決定木の一般的構造を示す図。
【図１４】図１２の遷移関数を並べ変えたものの内容を示す図。
【図１５】図１４の遷移関数において、状態空間が平坦化されたものの内容を示す図。
【図１６】図１５の遷移関数において、状態空間が定数及び変数のペアに変換されたものの内容を示す図。
【図１７】本発明の実施例における論理型プログラム比較手順の大まかな流れを示すフローチャート。
【符号の説明】
１：キーボード
２：表示装置
３：Ｉ／Ｏ制御回路
４：入力部
５：変換部
６：比較部
７：出力部
【図１】
0003582849.tif 000018
【図２】
0003582849.tif 000019
【図３】
0003582849.tif 000020
【図４】
0003582849.tif 000021
【図５】
0003582849.tif 000022
【図６】
0003582849.tif 000023
【図７】
0003582849.tif 000024
【図８】
0003582849.tif 000025
【図９】
0003582849.tif 000026
【図１０】
0003582849.tif 000027
【図１１】
0003582849.tif 000028
【図１２】
0003582849.tif 000029
【図１３】
0003582849.tif 000030
【図１４】
0003582849.tif 000031
【図１５】
0003582849.tif 000032
【図１６】
0003582849.tif 000033
【図１７】
0003582849.tif 000034