(57)【要約】      （修正有）【課題】自動定理証明装置によるソフトウェア仕様の証明が成功する可能性を向上する。【解決手段】自動定理証明装置は、プロセッサおよび記憶部を備え、記憶部にソフトウェア仕様の属する言語の構文規則と言語に対応する証明手続を格納し、ソフトウェア仕様の証明時に、構文規則を用いてソフトウェア仕様を構文解析することでソフトウェア仕様の属する言語を特定し、ソフトウェア仕様の属する言語からソフトウェア仕様を証明するための証明手続きを決定し、その証明手続きによってソフトウェア仕様を証明する。【選択図】図１
2011242956.tif 000002
【特許請求の範囲】
【請求項１】
形式言語で記述されるソフトウェア仕様を証明する自動定理証明装置であって、
プロセッサ、及び記憶部を備え、
前記記憶部は、前記ソフトウェア仕様の属する言語の構文規則、及び前記言語に対応する証明手続きを格納し、
前記プロセッサは、
前記構文規則を用いて前記ソフトウェア仕様を構文解析して、前記ソフトウェア仕様の属する言語を特定し、
前記ソフトウェア仕様の属する言語から、前記ソフトウェア仕様を証明するための証明手続きを決定し、
前記証明手続きによって、前記ソフトウェア仕様を証明する
ことを特徴とする自動定理証明装置。
【請求項２】
前記記憶部は、形式言語と同等の意味を持つが構文は異なる表層記法によって記述したソフトウェア仕様を、形式言語に変換する変換情報を格納し、
前記プロセッサは、前記表層記法で記述されるソフトウェア仕様を、形式言語で記述されるソフトウェア仕様に変換する
ことを特徴とする請求項１に記載の自動定理証明装置。
【請求項３】
前記記憶部は、前記表層記法で記述するソフトウェア仕様の属する言語に対応する証明手続きを格納し、
前記プロセッサは、前記表層記法で記述されるソフトウェア仕様を形式言語で記述されるソフトウェア仕様に変換する際に、前記ソフトウェア仕様の属する言語を特定し、
そのため、請求項１に記載の、形式言語で記述されるソフトウェアの構文解析を行わない、
ことを特徴とする請求項２に記載の自動定理証明装置。
【請求項４】
形式言語で記述されるソフトウェア仕様を証明する自動定理証明装置における自動定理証明方法であって、
前記自動定理証明装置は，プロセッサ、及び記憶部を備え、
前記記憶部は、前記ソフトウェア仕様の属する言語の構文規則、及び前記言語に対応する証明手続きを格納し、
前記プロセッサは、
前記構文規則を用いて前記ソフトウェア仕様を構文解析して、前記ソフトウェア仕様の属する言語を特定し、
前記ソフトウェア仕様の属する言語から、前記ソフトウェア仕様を証明するための証明手続きを決定し、
前記証明手続きによって、前記ソフトウェア仕様を証明する
ことを特徴とする自動定理証明方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ソフトウェア開発を支援する技術に関し、特に、ソフトウェア仕様を証明する技術に関する。
【背景技術】
【０００２】
従来、ソフトウェア仕様の正しさに関する形式的な証明は、自然言語又は図などによって記述されたソフトウェア仕様（以下、「自然言語仕様」）を形式言語によって記述された形式言語仕様に変換し、変換された形式言語仕様を証明する手順で行われている。
【０００３】
この形式言語仕様の証明手段として、計算機による自動定理証明装置が用いられる。特に一階述語論理の自動定理証明装置が主流であり、例えば、BやEvent Bなどの言語で記述した形式言語仕様の証明に用いられる。（非特許文献１、非特許文献２参照）
ところで、一階述語論理の論理体系は健全かつ完全である。即ち、誤りのない形式言語仕様は自動定理証明装置にて証明可能であり、かつ自動定理証明装置で証明できた形式言語仕様には誤りはないと言える。
【０００４】
一方で、一階述語論理においては論理式の証明可能性を機械的に判定できないことが知られている（以下、証明可能性を機械的に判定できることを決定可能、判定できないことを決定不能とも呼ぶ）。即ち、自動定理証明装置を使って形式言語仕様を証明しようとした場合に、当該形式言語仕様の証明の可否を有限時間内に示すことができない。
【０００５】
つまり、自動定理証明装置は誤りのない形式言語仕様を証明できる方法を提供するが、その手続きが有限時間内に終了する保証はなく、証明を成功できずに無限に動作し続ける可能性がある。また、そもそも形式言語仕様に誤りがある場合は、証明手続きは成功することなく無限に動作し続ける。
【０００６】
このように証明手続きが有限時間内に終了する保証はないため、現実の自動証明装置は証明手続きを中断する方法を備えている。例えば、制限時間によって証明手続きを中断する方法や、ユーザの判断により任意のタイミングで証明手続きを中断する方法がある。
【０００７】
以上より、誤りのある形式言語仕様を自動証明装置に入力した場合は、証明は終了せずに中断することになる。しかし誤りのない形式言語仕様を自動証明装置に入力した場合は、証明が成功する場合と、証明が終了せずに中断する場合とがある。
【０００８】
これを自動定理証明装置のユーザの視点でみると、自動定理証明装置による証明が（偶然）成功した場合には、形式言語仕様には誤りはないと判断できる。しかし、証明が成功する前に（制限時間により、あるいはたまりかねて）証明手続きを中断した場合は、当該形式言語仕様に誤りがあるのかどうか判断できない。
【０００９】
そのため、誤りのない形式言語仕様は短時間で簡単に証明できることが望ましい。なぜなら、誤りのない形式言語仕様が短時間で簡単に証明できるのであれば、証明が成功しなかった形式言語仕様には誤りがある可能性が高いからである。
【００１０】
そのため従来から、自動定理証明装置を用いたソフトウェア仕様の証明では，ユーザが証明の戦略を指定することで効率的に証明を行う方法や、証明の問題を効率的な解法アルゴリズムがある他の問題に置き換えて解くなどの方法が開示されている。（特許文献１参照）
一方、述語が表れない論理式（命題論理の論理式）や、引数を一つしか持たない述語（単項述語）からなる一階述語論理式は決定可能であることが知られている。
【先行技術文献】
【特許文献】
【００１１】
【特許文献１】特開２００５−４４３０３号公報
【非特許文献】
【００１２】
【非特許文献１】Event-B.org、"Event-B and the Rodin Platform"、[online]、平成21年1月20日検索、インターネット<URL：http://www.event-b.org/>
【非特許文献２】ClearSy、"Atelier B"、[online]、平成21年1月20日検索、インターネット<URL：http://www.atelierb.eu/index-en.php >
【発明の概要】
【発明が解決しようとする課題】
【００１３】
上述の通り、一階述語論理式の部分的な論理式は決定可能である。つまり、一階述語論理の文法に従って記述できる形式言語仕様には、有限時間内でその証明可能性を判定できる形式言語仕様も含まれる。
【００１４】
しかし従来技術では、決定可能な形式言語仕様と決定不能な形式言語仕様とを区別せずに、決定不能な形式言語仕様を証明するための手続きで、決定可能な形式言語仕様を証明している。そのため、決定可能な形式言語仕様を証明する際に、その証明手続きが終了しない可能性がある。あるいは、決定可能な形式言語仕様に対しては有限時間内で終了するような証明手続きを使っていても、制限時間などによって途中で証明手続きを中断してしまう可能性がある。
【００１５】
つまり、決定可能な形式言語仕様であるにも関わらず、自動定理証明装置を用いてその誤りの有無を判定できない場合があるという問題がある。
【００１６】
以上より、一階述語論理を始めとする決定不能な形式言語で記述した形式言語仕様を証明する自動定理証明装置において、入力された形式言語仕様が決定可能な場合は、その誤りの有無を有限時間内に判定できるようにすることが課題となる。
【００１７】
本発明の目的は、上記課題に対処し、決定不能な論理式を記述できる形式言語で仕様を記述した場合に、当該形式言語仕様が決定可能であればその仕様に誤りがあるかを機械的に判定できるようにするための技術を提供することである。
【課題を解決するための手段】
【００１８】
そのため、本発明は、形式言語で記述されるソフトウェア仕様を証明する自動定理証明装置であって、前記ソフトウェア仕様の属する言語の構文規則、及び前記言語に対応する証明手続きを格納し、前記構文規則を用いて前記ソフトウェア仕様を構文解析して、前記ソフトウェア仕様の属する言語を特定し、前記ソフトウェア仕様の属する言語から、前記ソフトウェア仕様を証明するための証明手続きを決定し、前記証明手続きによって、前記ソフトウェア仕様を証明することを特徴とする自動定理証明装置を提供する。
【発明の効果】
【００１９】
本発明の一形態によれば、ソフトウェア仕様の正しさを形式的に証明する際において、決定不能な論理式を記述できる十分な記述力を持つ形式言語で記述した形式言語仕様を，その形式言語仕様に適した方法で証明を行うため，記述した形式言語仕様が決定可能であれば、その仕様に誤りがあるかどうかを、自動定理証明装置を用いて人手を介さずに有限時間内に判定できる。
【００２０】
これにより、ソフトウェア仕様に誤りがあるかを判定できる可能性が向上する。
【図面の簡単な説明】
【００２１】
【図１】自動定理証明装置の構成例を示すブロック図である。
【図２】自動定理証明装置のハードウェア構成例を示す図である。
【図３】入力仕様保持部が保持する表層仕様の例を示す図である。
【図４】形式言語仕様保持部が保持する形式言語仕様の例を示す図（１）である
【図５】形式言語仕様保持部が保持する形式言語仕様の例を示す図（２）である。
【図６】表層記法保持部が保持する表層記法の定義の例を示す図である。
【図７】構文規則保持部が保持する構文規則の第１の例を示す図である。
【図８】構文規則保持部が保持する構文規則の第２の例を示す図である。
【図９】自動定理証明装置によってソフトウェア仕様を証明する手順例を示すフローチャートである。
【発明を実施するための形態】
【００２２】
以下、本発明の実施の一形態を、図面を参照しながら詳細に説明する。
【００２３】
本実施形態は、自動定理証明装置に適用される。本実施形態では、入力された形式言語仕様が前記形式言語のどの部分集合（以下、言語の部分集合を部分言語と呼ぶ）に属するかを構文解析によって特定し、その属する言語に応じて証明手続きの手順や、証明に使う推論規則、または証明の制限時間設定を変更する。前記証明手続きの手順、証明に使う推論規則、及び証明の制限時間設定は、対応する言語の証明を行うための最適な設定を用意しておく。
【００２４】
よって本実施形態によれば、決定不能な論理式を記述できる十分な記述力を持つ形式言語で形式言語仕様を記述でき、記述した形式言語仕様が決定可能な言語に属する場合には、形式言語仕様に誤りがあるかどうかを自動定理証明装置により有限時間内に判定できる。
【００２５】
さらに、記述した形式言語仕様を証明する上で最適な（必要最小限の）推論規則を使用できるため、不要あるいは冗長な推論は行わない。よって、証明にかかる時間を短縮できる。
【００２６】
また本実施形態では、自動定理証明装置の入力として、形式言語仕様以外にも表などの形式で記述した仕様（以下、表などの形式の記法を表層記法、表層記法で記述した仕様を表層仕様とも呼ぶ）を受け付ける。自動定理証明装置は、表層仕様を受け付けた後、仕様解析によってその表層記法を特定し、表層仕様を形式言語仕様へと変換する。
【００２７】
よって本実施形態によれば、形式言語よりも記述や解読が容易な表層言語形式でソフトウェア仕様を記述できる。
【００２８】
さらに本実施形態では，表層記法に対して、その表層記法で記述可能な、形式言語の部分言語を予め対応付けておく。すると表層記法で仕様を記述した場合は、仕様解析によって表層記法を特定した時点で、その仕様が属する部分言語を特定できる。つまり、表層仕様を変換して得た形式言語仕様に対しては、その形式言語仕様が属する部分言語を特定するための構文解析を省略できる。
【００２９】
よって本実施形態によれば、表層言語形式でソフトウェア仕様を記述した場合に、前記ソフトウェア仕様に対する仕様解析あるいは構文解を重複して行うことはないため、効率的にソフトウェア仕様の証明が行える。
【００３０】
図１は、本実施形態における自動定理証明装置２０１の構成例を示すブロック図である。
【００３１】
自動定理証明装置２０１は、入力部１０１、入力仕様保持部１０２、表層仕様解析部１０３、表層仕様保持部１０５、表層仕様変換部１０４、変換情報保持部１１２、形式言語仕様保持部１０６、構文解析部１０７、構文規則保持部１０８、証明部１０９、推論規則保持部１１０、及び出力部１１１を含む。
【００３２】
入力部１０１は、検証対象のソフトウェア仕様を受け付け、前記ソフトウェア仕様を入力仕様保持部１０２に登録する。
【００３３】
表層記法解析部１０３は、それぞれ入力仕様保持部１０２からソフトウェア仕様を、表層記法保持部１０５から前記ソフトウェア仕様解析のための表層記法定義を取得する。前記表層記法定義は、表層記法の表記方法や構文規則に加え，その表層記法で記述可能な形式言語の部分言語を識別する言語識別情報を含む。表層記法解析部１０３は前記ソフトウェア仕様を、前記表層記法定義を用いて解析する。前記解析においては、まず前記ソフトウェアが表層記法で記述されているか、あるいは形式言語で記述されているかを判別する。さらに前記ソフトウェア仕様が表層記法で記述されていることが分かったら、その表層記法を特定する。
【００３４】
前記解析の結果、前記ソフトウェア仕様が形式言語で記述されていた場合は、前記ソフトウェア仕様を形式言語仕様として形式言語仕様保持部１０６に登録する。
【００３５】
前記解析の結果、前記ソフトウェア仕様が表層記法で記述されていた場合は、前記表層記法を識別するための表層記法識別情報と、前記表層記法に対応する言語識別情報を、前記表層仕様で記述されたソフトウェア仕様（表層仕様）に追加する。その後、前記表層仕様を表層仕様変換部１０４に渡す。
【００３６】
表層仕様変換部１０４は、表層記法解析部１０３から表層仕様を受け取り、受け取った表層仕様が含む表層記法識別情報から、記述に使われている表層記法を識別する。そして、識別した表層記法に対応する表層記法変換情報を、変換情報保持部１１２から取得する。さらに取得した表層記法変換情報を使って、前記表層仕様を形式言語仕様に変換する。変換によって得た形式言語仕様は、もとの表層仕様が含んでいた言語識別情報を含むものとする。表層仕様変換部１０４は、変換によって得た形式言語仕様を形式言語仕様保持部１０６に登録する。
【００３７】
構文解析部１０７は、形式言語仕様保持部１０６を参照し、言語識別情報を含まない形式言語仕様を取得する。また構文規則保持部１０８から、言語の構文規則を取得する。この構文規則は形式言語の部分言語ごとに定義されるもので、形式言語仕様がある構文規則に従って記述されていれば、その形式言語仕様はその構文規則に対応する言語に属すると言える。そこで構文解析部１０７は、形式言語仕様保持部１０６から取得した前記形式言語仕様を、構文規則保持部１０８から取得した前記構文規則を使って構文解析し、前記形式言語仕様が属する言語を特定する。そして、特定した言語を識別する言語識別情報を前記形式言語仕様に追加し、形式言語仕様保持部１０６に再登録する。
【００３８】
証明部１０９は、形式言語仕様保持部１０６から言語識別情報を含む形式言語仕様を取得する。そして、前記言語識別情報の示す言語のための推論規則を、推論規則保持部１１０から取得する。例えば、言語識別情報が「命題論理」であれば命題論理の推論規則を、「一階述語論理」であれば一階述語論理の推論規則を取得する。ところで、（少なくとも自然演繹体系においては）一階述語論理の推論規則は命題論理の推論規則を包含するため、命題論理に属する言語は一階述語論理の推論規則でも証明できる。しかし、一階述語論理の推論規則は命題論理の言語の推論には不要な規則も含んでいる。そのため、機械的な証明手続きにおいては，命題倫理の言語の証明には命題論理の推論規則のみを使用した方が時間効率が良い。
【００３９】
また証明部１０９は、前記言語識別情報に応じて、証明手続きの手順や制限時間設定を変更する。例えば言語識別情報が「命題論理」であれば、証明の制限時間を無限に設定し、証明手続きを途中で中断することのないようにする。これにより、形式言語仕様が命題論理の言語に属する場合はその誤りの有無を有限時間内に判定できる。また例えば言語識別情報が「単項一階述語論理」の場合は、証明手順も変更する。具体的には、量化子の導入あるいは除去の際に使用するパラメータの個数を、当該形式言語仕様から求められる有限個数に限定して証明を行う。有限個数のパラメータを使った証明手順は有限時間内に終了するため、手順終了時まで証明できなかった形式言語仕様は誤りのある形式言語仕様と判定する。この証明手順によって、形式言語仕様の誤りの有無を有限時間内に判定できる。
【００４０】
そして証明部１０９は、取得した推論規則と設定した制限時間、及び設定した証明手順によって、前記形式言語仕様の証明手続きを実行する。証明の結果やログは、出力部１１１を介して画面表示する。
【００４１】
効率的な証明手続きとしては導出法やタブローの方法が代表的で、これらの方法を用いてもよい。導出法を用いる場合は、上述の推論規則は導出規則に相当する。同様にタブローの方法を用いる場合は、上述の推論規則はタブローの展開規則に相当する。
【００４２】
出力部１１１は、証明部１０９から証明の結果やログを表すデータを受け取り、画面表示する。
【００４３】
図２は、本実施形態における自動定理証明装置のハードウェア構成例を示す図である。
【００４４】
自動定理証明装置２０１は、ＣＰＵ２０２、メモリ２０３、外部記憶装置２０４、表示装置２０５、入力装置２０６、及び外部媒体入出力装置２０７を備える。
【００４５】
ＣＰＵ２０２は、メモリ２０３に記憶されたプログラムを実行することによって、各種処理を実行する。メモリ２０３は、ＣＰＵ２０２のワークエリアとして機能し、プログラム及びプログラムの実行に必要なデータを記憶する。具体的には、表層記法解析部１０３、表層仕様変換部１０４、構文解析部１０７、及び証明部１０９を構成するプログラムが記憶され、同時に入力仕様保持部１０２、表層記法保持部１０５、変換情報保持部１１２、形式言語仕様保持部１０６、構文規則保持部１０８、及び推論規則保持部１１０の保持するデータが記憶される。
【００４６】
外部記憶装置２０４は、各種データを格納する。外部記憶装置２０４は、例えば、ハードディスク装置などである。具体的には、入力仕様保持部１０２、表層記法保持部１０５、変換情報保持部１１２、形式言語仕様保持部１０６、構文規則保持部１０８、及び推論規則保持部１１０が格納される。
【００４７】
あるいは、表層記法解析部１０３、表層仕様変換部１０４、構文解析部１０７、及び証明部１０９を構成するプログラムの少なくとも一部についても、外部記憶装置２０４に格納され、各種処理実行の際にＣＰＵ２０２がメモリ２０３へ読み出してプログラムを実行することとしてもよい。また各プログラムは、あらかじめ、メモリ２０３または外部記憶装置２０４に格納されていても良いし、必要に応じ、利用可能な媒体を介して、他の装置からメモリ２０３または外部記憶装置２０４に導入されてもよい。媒体とは、例えば、外部媒体入出力装置２０７に着脱可能な記憶媒体、または、ネットワークや、ネットワークを伝搬する搬送波やデジタル信号などの通信媒体を指す。
【００４８】
表示装置２０５は、プログラムの処理結果などを表示する。表示装置２０５は、例えば、ディスプレイなどである。入力装置２０６は、処理の実行指示及び処理に必要な情報の入力などを利用者から受け付ける。入力装置２０６は、例えば、キーボード及びマウスなどである。
【００４９】
外部媒体入出力装置２０７は、外部媒体と、外部記憶装置２０４に格納されているデータなどの入出力を行う。外部媒体は、外部媒体入出力装置２０７に着脱可能で可搬性のある記憶媒体であり、外部媒体出力装置２０７は、外部媒体に読み書き可能なドライブ装置などである。
【００５０】
図３は、入力仕様保持部が保持する表層仕様の例を示す図である。
【００５１】
テーブル３０１、テーブル３０２、及び矢印３０３によってソフトウェアの仕様を表している。
【００５２】
テーブル３０１、及びテーブル３０２は、表形式の仕様記述要素であり、表によって１つの処理を表している。矢印３０３はテーブルの表す処理の実行順序を表しており、テーブル３０１の表す処理を実行した後、テーブル３０２の表す処理を実行することを意味する。
【００５３】
テーブル３０１が含む条件３０４、及び操作３０５は、テーブル３０１の処理内容を定義する項目である。テーブル３０１は、条件３０４の条件が成立した場合に、操作３０５の内容を実行するという処理を表す。テーブル３０１の例では、「approachというデータ項目の値がonで、かつinternalというデータ項目の値がoffの場合、lockというデータ項目の値をlockedに設定し、さらにsignalというデータ項目の値をreverseに設定する」という処理を表す。
【００５４】
図４及び図５は、形式言語仕様保持部が保持する形式言語仕様の例を示す図である
本例は図３の表層仕様をEvent-B言語で記述したものである。モデル４０２とコンテクスト５０１によって、図３の表層仕様が示すソフトウェア仕様を表している。
【００５５】
言語識別情報４０１は、表層記法解析部１０３、あるいは構文解析部１０７が追加する情報で、モデル４０２及びコンテクスト５０１の仕様がどの言語に属しているかを表している。
【００５６】
図６は、表層記法保持部が保持する表層記法定義の例を示す図である。
【００５７】
表記方法６０１は表によるソフトウェア仕様表記方法を定義しており、括弧（＜＞）で括っている記入項目に文字列を記入することで仕様を記述できる。
【００５８】
構文規則６０２は、前記記入項目に記入する文字列の構文規則を表している。本例では前記構文規則を、BNF記法（バッカス・ナウア記法）を用いて定義している。
【００５９】
言語６０３は，表記方法６０１及び構文規則６０２の定義する表層記法に対応する言語を定義している。形式言語仕様が表記方法６０１及び構文規則６０２に従って記述されるならば、その形式言語仕様は言語６０３に属することを意味する。
【００６０】
図７は、構文規則保持部が保持する構文規則の第１の例を示す図である。
【００６１】
構文規則７０１は、形式言語Event-Bの部分言語の構文規則を表しており、図４及び図５にて示した形式言語仕様は構文規則７０１に従って記述されている。
【００６２】
言語７０２は、構文規則７０１に対応する言語を定義している。形式言語仕様が構文規則７０１に従って記述されるならば、その形式言語仕様は言語７０２に属することを意味する。
【００６３】
図８は、構文規則保持部が保持する構文規則の第２の例を示す図である。
【００６４】
構文規則８０１は、形式言語Event-Bの部分言語の構文規則を表している。
【００６５】
言語８０２は、構文規則８０１に対応する言語を定義している。
【００６６】
図７の第１の例と図８の第２の例との違いは構文８０３の部分で、図８では、図７で許されていなかった∀や∃という量化子を記述できる。
【００６７】
ところで、図４及び図５にて示した形式言語仕様は構文規則７０１に従っていると述べたが、前記形式言語仕様は構文規則８０１にも違反していない。これは、構文規則８０１が構文規則７０１を包含する規則であることが原因で、そのため構文規則７０１に従って記述した形式言語仕様は、必ず構文規則８０１にも従う。
【００６８】
つまり、図４及び図５にて示した形式言語仕様は、言語７０２に属すると同時に、言語７０２の全体を包含する言語８０２にも属することになる。このような場合自動定理証明装置は、より小さな言語である言語７０２に属すると判定する。よって図４及び図５にて示した形式言語仕様は、言語７０２に属する
図９は、自動定理証明装置によってソフトウェア仕様を証明する手順例を示すフローチャートである。以下に示す処理は、自動定理証明装置２０１の備えるＣＰＵ２０２が、メモリ２０３で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。
【００６９】
ＣＰＵ２０２は、入力部１０５を実行することによって、ソフトウェア仕様の入力を受け付け、前記ソフトウェア仕様を入力仕様保持部１０２に登録する。（ステップ９０１）。
【００７０】
ＣＰＵ２０２は、表層記法解析部１０３を実行することによって、入力仕様保持部１０２から前記ソフトウェア仕様を取得する。さらに表層記法保持部１０５から、前記ソフトウェア仕様の解析のための表層記法定義を取得する。そして表層記法解析部１０３は、前記ソフトウェア仕様を前記表層記法定義に基づいて解析し、前記ソフトウェア仕様の記述に使われている記法を特定する（ステップ９０２）。
【００７１】
ＣＰＵ２０２は、ステップ９０２の結果、前記ソフトウェアが形式言語で記述されていることが分かった場合はステップ９０４を実行する。前記ソフトウェアが表層記法で記述されていることが分かった場合はステップ９０７を実行する（ステップ９０３）。
【００７２】
ＣＰＵ２０２は、表層記法解析部１０３を実行することによって、形式言語で記述されたソフトウェア仕様である形式言語仕様を形式言語仕様保持部１０６に登録する（ステップ９０４）。
【００７３】
ＣＰＵ２０２は、構文解析部１０７を実行することによって、形式言語仕様保持部１０６から、言語識別情報を含まない形式言語仕様を取得する。同時に構文規則保持部１０８から、言語の構文規則を取得する。さらに、取得した前記形式言語仕様を前記構文規則によって構文解析し、前記形式言語仕様が属する言語を特定する（ステップ９０５）。
【００７４】
構文解析部１０７は、ステップ９０５で特定した言語を識別する言語識別情報を前記形式言語仕様に追加し、形式言語仕様保持部１０６に再登録する。その後ステップ９０９を実行する（ステップ９０６）。
【００７５】
ＣＰＵ２０２は、表層記法解析部１０３を実行することによって、ステップ９０２で特定した表層記法を識別するための表層記法識別情報と、前記表層記法に対応する言語識別情報を、前記表層仕様で記述されたソフトウェア仕様である表層仕様に追加する。その後、前記表層仕様を表層仕様変換部１０４に渡す（ステップ９０７）。
【００７６】
ＣＰＵ２０２は、表層仕様変換部１０４を実行することによって、表層記法解析部１０３から表層仕様を受け取り、受け取った表層仕様が含む表層記法識別情報から、記述に使われている表層記法を識別する。また、変換情報保持部１１２から、識別した表層記法に対応する表層記法変換情報を取得する。さらに、取得した表層記法変換情報を使って前記表層仕様を形式言語仕様に変換する。そして、変換によって得た形式言語仕様を形式言語仕様保持部１０６に登録する。その後ステップ９０９を実行する（ステップ９０８）。
【００７７】
ＣＰＵ２０２は、証明部１０９を実行することによって、形式言語仕様保持部１０６から言語識別情報を含む形式言語仕様を取得する。そして、前記言語識別情報の示す言語のための推論規則を、推論規則保持部１１０から取得する。また前記言語識別情報に応じて、証明手続きの手順や制限時間設定を変更する。そして、取得した推論規則と設定した制限時間、及び設定した証明手順によって、前記形式言語仕様の証明手続きを実行する。
【００７８】
以上のようにして、ソフトウェア仕様を表す形式言語仕様に対して、その形式言語の属する言語に応じて適切な推論規則、制限時間、及び証明手順を用いて前記形式言語仕様の証明を行う証明手段と、形式言語とは異なる表層記法で記述したソフトウェア仕様（表層仕様）を形式言語仕様に変換する手段と、前記表層仕様から変換した形式言語仕様の証明を効率的に行う手段を提供する、自動定理証明装置を提供できる。
【００７９】
これらの手段を使ってソフトウェア仕様を検証することで、ソフトウェア仕様に矛盾のないこと、あるいはソフトウェア仕様が所定の性質を満足することを保証できる可能性が向上する。同様に、ソフトウェア仕様に矛盾のあること、あるいはソフトウェア仕様が所定の性質を満足しないこと保証できる可能性が向上する。
【符号の説明】
【００８０】
１０１    入力部
１０２    入力仕様保持部
１０３    表層記法解析部
１０４    表層仕様変換部
１０５    表層仕様保持部
１０６    形式言語仕様保持部
１０７    構文解析部
１０８    構文規則保持部
１０９    証明部
１１０    推論規則保持部
１１１    出力部
１１２    変換情報保持部
【図１】
2011242956.tif 000003
【図２】
2011242956.tif 000004
【図３】
2011242956.tif 000005
【図４】
2011242956.tif 000006
【図５】
2011242956.tif 000007
【図６】
2011242956.tif 000008
【図７】
2011242956.tif 000009
【図８】
2011242956.tif 000010
【図９】
2011242956.tif 000011