(57)【特許請求の範囲】
【請求項１】
システムの動作仕様を記述した１以上の形式言語文から成る形式言語仕様記述の更新処理を行う、形式言語仕様記述更新部と、
前記動作仕様が満たすべき条件である検証性質を形式言語で記述した検証性質記述の更新処理を行う検証性質更新部と、を有し、
前記形式言語仕様記述更新部は、前記動作仕様が前記検証性質を満たさない場合の前記形式言語仕様記述の実行系列のうちユーザから選択された実行系列を表す除外反例に基づいて、
前記形式言語仕様記述を構成する前記形式言語文の実行の過程で前記除外反例に含まれる前記形式言語文が実行された時に、前記形式言語文が実行されたことを時系列で記録するための処理を前記形式言語で記述した、トレース挿入用記述を作成し、
前記トレース挿入用記述を前記形式言語仕様記述に挿入することで、前記形式言語仕様記述を更新し、
前記検証性質更新部は前記トレース挿入用記述及び前記除外反例を用いて、
前記検証性質記述を、「前記検証性質が成立しなければ、前記除外反例の示す順序で前記形式言語仕様記述を構成する前記形式言語文が実行された」という性質の記述に書き換える、
システム仕様検証支援装置。
【請求項２】
前記除外反例は、
前記形式言語仕様記述に含まれる形式言語文と、前記形式言語文の前記形式言語仕様記述内の行番号との組み合わせである除外反例文を、１以上含む、
請求項１に記載のシステム仕様検証支援装置。
【請求項３】
前記トレース挿入用記述は、
前記除外反例文の実行を記録するためのトレース配列の定義と、
前記除外反例文毎に定められた定数の定義と、
前記除外反例文に含まれる前記形式言語文が実行された時、前記トレース配列に前記除外反例文を表す定数を代入する処理と、
を含む、請求項２に記載のシステム仕様検証支援装置。
【請求項４】
前記システム仕様検証支援装置はさらに、
前記形式言語仕様記述と前記検証性質記述を入力として受け付けて、前記形式言語仕様記述に記述された前記動作仕様の検証を行い、前記動作仕様が前記検証性質を満たさない場合の前記形式言語仕様記述の実行系列を反例として出力する検証部を有する、
請求項２または３に記載のシステム仕様検証支援装置。
【請求項５】
前記システム仕様検証支援装置は、
前記検証部の出力した前記反例を用いて前記除外反例を作成する除外反例作成部を、
さらに有する、請求項４に記載のシステム仕様検証支援装置。
【請求項６】
前記除外反例作成部は、前記反例に含まれる１以上の形式言語文に対する編集入力を受け付けることで、前記反例に含まれる１以上の形式言語文を任意の順に組み合わせた実行系列を、前記除外反例として作成する、
請求項５に記載のシステム仕様検証支援装置。
【請求項７】
前記システム仕様検証支援装置はさらに、
前記形式言語仕様記述を構成する形式言語文の意味を説明する自然言語文の入力を受け付けて、前記検証部が前記反例を出力する際に、前記実行系列とともに前記自然言語文が出力されるように前記形式言語仕様記述を更新する自然言語文挿入部と、
前記反例から、前記自然言語文を抽出することで、自然言語反例を作成する自然言語反例作成部と、
前記自然言語反例から前記除外反例を作成する自然言語反例向け除外反例作成部、
を有する、請求項４に記載のシステム仕様検証支援装置。
【請求項８】
前記自然言語反例向け除外反例作成部は、前記自然言語反例を構成する自然言語文に対する編集入力を受け付け、前記自然言語文を任意に組み合わせた自然言語の実行系列を前記自然言語反例として作成する、
請求項７に記載のシステム仕様検証支援装置。
【請求項９】
システムの動作仕様を記述した１以上の形式言語文から成る形式言語仕様記述の更新処理を行う、形式言語仕様記述更新部と、
前記動作仕様が満たすべき条件である検証性質を形式言語で記述した検証性質記述の更新処理を行う検証性質更新部と、を有する計算機が実行する、システム仕様検証支援方法であって、
前記計算機が、
前記動作仕様が前記検証性質を満たさない場合の前記形式言語仕様記述の実行系列のうちユーザから選択された実行系列を表す除外反例に基づいて、
前記形式言語仕様記述を構成する前記形式言語文の実行の過程で前記除外反例に含まれる前記形式言語文が実行された時に、前記形式言語文が実行されたことを時系列で記録するための処理を前記形式言語で記述した、トレース挿入用記述を作成し、前記トレース挿入用記述を前記形式言語仕様記述に挿入することで、前記形式言語仕様記述を更新する工程と、
前記トレース挿入用記述及び前記除外反例を用いて、前記検証性質記述を、「前記検証性質が成立しなければ、前記除外反例の示す順序で前記形式言語仕様記述を構成する前記形式言語文が実行された」という性質の記述に書き換える工程と、
を実行する、システム仕様検証支援方法。
【請求項１０】
前記除外反例は、前記形式言語仕様記述に含まれる形式言語文と、前記形式言語文の前記形式言語仕様記述内の行番号との組み合わせである除外反例文を、１以上含み、
前記トレース挿入用記述は、
前記除外反例文の実行を記録するためのトレース配列の定義と、
前記除外反例文毎に定められた定数の定義と、
前記除外反例文に含まれる前記形式言語文が実行された時、前記トレース配列に前記除外反例文を表す定数を代入する処理と、
を含む、請求項９に記載のシステム仕様検証支援方法。
【請求項１１】
前記形式言語仕様記述を更新する工程の前に、
前記形式言語仕様記述と前記検証性質記述を入力として受け付けて、前記形式言語仕様記述に記述された前記動作仕様の検証を行い、前記動作仕様が前記検証性質を満たさない場合の前記形式言語仕様記述の実行系列を反例として出力する工程を実行する、
請求項９または１０に記載のシステム仕様検証支援方法。
【請求項１２】
前記反例を用いて前記除外反例を作成する工程をさらに有する、
請求項１１に記載のシステム仕様検証支援方法。
【請求項１３】
前記除外反例を作成する工程では、前記反例に含まれる１以上の形式言語文に対する編集入力を受け付けることで、前記反例に含まれる１以上の形式言語文を任意の順に組み合わせた実行系列を、前記除外反例として作成する、
請求項１２に記載のシステム仕様検証支援方法。
【請求項１４】
前記形式言語仕様記述を構成する形式言語文の意味を説明する自然言語文の入力を受け付けて、前記動作仕様が前記検証性質を満たさない場合の前記形式言語仕様記述の実行系列を出力する工程において、前記実行系列とともに前記自然言語文が出力されるように前記形式言語仕様記述を更新する工程と、
前記反例から、前記自然言語文を抽出することで、自然言語反例を作成する工程と、
前記自然言語反例から前記除外反例を作成する工程と、
を実行する、請求項１１に記載のシステム仕様検証支援方法。
【請求項１５】
前記自然言語反例を作成する工程では、前記自然言語反例を構成する自然言語文に対する編集入力を受け付け、前記自然言語文を任意に組み合わせた自然言語の実行系列を前記自然言語反例として作成する、
請求項１４に記載のシステム仕様検証支援方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、システム仕様の検証を支援する技術に関する。
【背景技術】
【０００２】
システムの不具合、たとえばソフトウェアシステムの不具合の原因の一つに、設計したソフトウェアの仕様誤りがある。仕様誤りを検出するためには、形式手法による検証が有効である。形式手法によるソフトウェア仕様の検証では、まず数学的意味を持つ形式言語を用いてシステムの動作仕様を示す状態遷移系のモデル、およびそのシステムの動作仕様が満たすべき性質（検証性質）を記述する。そして、形式言語で記述されたモデルの記述（以下、これを形式言語仕様記述と呼ぶ）が、同じく形式言語で記述された性質（以下、検証性質記述と呼ぶ）を満たすかを、数学的手法に基づいて検証する。
【０００３】
形式手法のうちモデル検査法と呼ばれる種類の手法では、上記検証を機械的に実行できる。そのため、多くのモデル検査法において、検証を自動化するためのツールが開発されている。例えば、形式言語Promelaにて記述した形式言語仕様記述および検証性質記述は、SPINと呼ばれる検証ツールにて自動検証可能である。
【０００４】
モデル検査法における検証ツールは、形式言語仕様記述および検証性質記述を入力として受け付ける。そして検証の結果、上記形式言語仕様記述が上記検証性質記述を満たさないと判明した場合は、検証ツールは、「形式言語仕様は検証性質を違反する」ことを示すメッセージとともに、その性質違反に至るまでの実行系列を出力する。この実行系列は、反例と呼ばれる。検証ツールは、検証対象の形式言語仕様記述を検査する過程において、一つの反例を検出次第、検証を終了してその反例を出力する。検証者は、検証ツールが出力した反例を解読することで、どのような場合に上記性質違反が発生するかを認識できるため、上記反例に基づいてシステム仕様の修正を行える。
【０００５】
ところで、形式言語は実際のシステムの振る舞いを抽象的かつ模式的に表現可能であることから、形式言語仕様記述の表すシステム仕様が、実際のシステムの振る舞いを忠実に表していない場合がある。その場合、実際のシステムでは起こり得ない実行系列が、反例として出力される場合がある。そのような反例は、偽反例と呼ばれる。
【０００６】
上記偽反例の存在を考慮すると、検証者は反例が出力された場合に、まずその反例が偽反例か否かを判断する必要がある。そして、出力された反例は偽反例ではない反例（以下、正反例と呼ぶ）と判断した場合は、ソフトウェア仕様の修正を行う。逆に、出力された反例は偽反例と判断した場合には、実際のシステムの振る舞いと一致するように形式言語仕様記述を適切に詳細化することで、上記偽反例が反例として出力されないようにする必要がある。形式言語仕様記述を適切に詳細化できた場合は、再検証の結果、上記偽反例とは異なる反例が出力されるか、あるいは「形式言語仕様は検証性質を満たす」ことを示すメッセージが出力される。
【０００７】
このように検証の結果、偽反例が出力された場合には、当該偽反例が出力されないように適切に形式言語仕様記述を詳細化する必要がある。しかし、偽反例の内容に基づく形式言語仕様記述の詳細化は、人手によって行う必要があるため、大量の偽反例を含む形式言語仕様記述を対象とした場合、多くの手間と時間がかかるという問題がある。この問題に対処するため、特許文献１では、人手で形式言語仕様記述を詳細化せずに偽反例を除外するための方法を開示している。この方法によれば、出力された偽反例に基づいて検証性質を修正する装置を提供することで、人手で形式言語仕様記述を修正せずとも、偽反例を除外できるようになる。
【先行技術文献】
【特許文献】
【０００８】
【特許文献１】特開２０１０−１２８５１３号公報
【発明の概要】
【発明が解決しようとする課題】
【０００９】
しかしながら、上記特許文献１に開示の方法では、ある条件が常に成立し続ける、あるいは常に成立しないという特定の性質を持つ偽反例のみを除外できる。詳細には、「異常状態（到達してはいけない状態）に到達するための条件が常に成立する偽反例」、および「正常状態（到達すべき状態）に到達するための条件が全く成立しない偽反例」のみを除外できる。即ち、特許文献１に開示の方法では、上記以外の偽反例は除外できないという課題がある。実際のシステムの仕様では、これら以外の偽反例も多く存在する。また偽反例の内容は、検証対象のシステムの仕様やユーザ（システム設計者）のニーズによって異なるため、特許文献１に開示の方法では、多くの場合において（上記以外の偽反例が出力された場合）、人手での形式言語仕様記述の詳細化が必要になる。
【課題を解決するための手段】
【００１０】
開示するシステム仕様検証支援装置は、システムの動作仕様を記述した１以上の形式言語文から成る形式言語仕様記述の更新処理を行う、形式言語仕様記述更新部と、検証性質を形式言語で記述した検証性質記述の更新処理を行う検証性質更新部とを有する。形式言語仕様記述更新部は、ユーザから与えられた除外反例に基づいて、形式言語仕様記述の実行過程において、除外反例に含まれる形式言語文が実行された時に、その旨を時系列で記録するための処理を形式言語で記述したトレース挿入用記述を作成し、トレース挿入用記述を前記形式言語仕様記述に挿入することで形式言語仕様記述を更新する。また検証性質更新部は、トレース挿入用記述及び除外反例を用いて、検証性質記述を「前記検証性質が成立しなければ、前記除外反例の示す順序で前記形式言語仕様記述を構成する前記形式言語文が実行された」という性質の記述に書き換える。
【発明の効果】
【００１１】
開示する偽反例除外支援装置によれば、任意の偽反例を除外できるようになるため、システム仕様の検証における人手での作業量を削減し、システム仕様の不具合検出にかかる作業時間および作業工数を削減することができる。
【図面の簡単な説明】
【００１２】
【図１】実施例１に係る偽反例除外支援装置の構成例を示すブロック図である。
【図２】偽反例除外支援装置のハードウェア構成例を示す図である。
【図３】形式言語仕様記述とその検証性質記述の例である。
【図４】言語間対応関係保持部が保持する言語間対応関係の例である。
【図５】自然言語文挿入部によって自然言語文を反例に出力するように形式言語仕様記述を更新した結果の例である。
【図６】自然言語文挿入部の手順例を示すフローチャートである。
【図７】自然言語文挿入部における自然言語文挿入画面の例である。
【図８】検証部が出力し、反例保持部に保持する反例の例である。
【図９】除外反例作成部が作成する除外反例である。
【図１０】除外反例作成部の手順例を示すフローチャートである。
【図１１】除外反例作成部における除外反例作成画面の例である。
【図１２】除外反例に基づき、形式言語仕様記述更新部が更新した形式言語仕様記述の例である。
【図１３】形式言語仕様記述更新部の手順例を示すフローチャートである。
【図１４】除外反例に基づき、検証性質更新部が更新した検証性質記述の例である。
【図１５】検証性質更新部の手順例を示すフローチャートである。
【図１６】実施例２に係る偽反例除外支援装置の構成例を示すブロック図である。
【図１７】自然言語反例作成部が作成する自然言語反例の例である。
【図１８】自然言語反例作成部の手順例を示すフローチャートである。
【図１９】自然言語反例向け除外反例作成部の手順例を示すフローチャートである。
【図２０】自然言語反例向け除外反例作成部における自然言語反例の編集画面の例である。
【発明を実施するための形態】
【００１３】
以下、本発明のいくつかの実施形態について、図面を参照しながら説明する。
【実施例１】
【００１４】
図１は、実施例１におけるシステム仕様検証支援装置（偽反例除外支援装置）２０１の構成例を示すブロック図である。
【００１５】
偽反例除外支援装置２０１は、編集部１０１、自然言語文挿入部１０４、検証部１０６、除外反例作成部１１０、形式言語仕様記述更新部１１２、及び検証性質更新部１１３、の機能ブロックを含む。また偽反例除外支援装置２０１は、検証性質保持部１０２、形式言語仕様記述保持部１０３、言語間対応関係保持部１０５、反例保持部１０７、除外反例保持部１１１、の記憶部を有する。偽反例除外支援装置２０１は、ＣＰＵ、メモリ、入出力装置を有するコンピュータ上で実現される。上記各処理部は、ＣＰＵによって処理が実行され、各保持部はメモリに設けられる。
【００１６】
編集部１０１は、ユーザからの入力に従って、形式言語仕様記述及び検証性質記述を編集し、編集された形式言語仕様記述を形式言語仕様記述保持部１０３に格納し、また編集された検証性質記述を検証性質保持部１０２に格納する。編集部１０１はたとえば、公知の計算機上で稼働するテキストエディタでもよい。
【００１７】
自然言語文挿入部１０４は、形式言語仕様記述保持部１０３に保持している形式言語仕様記述について、上記形式言語仕様記述を構成する任意の形式言語文に対して、その意味を説明する自然言語文の入力を受け付ける。そして自然言語文挿入部１０４は、入力された自然言語文を反例に出力するように上記形式言語仕様記述を更新する。その際自然言語文挿入部１０４は、上記形式言語文と上記自然言語文との対応関係を、言語間対応関係保持部１０５に登録する。
【００１８】
検証部１０６は、形式言語仕様記述保持部１０３に保持している形式言語仕様記述、および検証性質保持部１０２に保持している検証性質記述を取得し、モデル検査法による検証を実行する。検証の結果、上記形式言語仕様記述が上記検証性質記述の示す性質を満たさないことが判明した場合は、検証部１０６は反例を出力しその反例を反例保持部１０７に登録する。検証部１０６は一例として、SPINなどの公知のモデル検査ツールである。
【００１９】
除外反例作成部１１０は、反例保持部１０７に保持している反例を取得し、上記反例を構成する形式言語文の選択をユーザから受け付けることで、選択された形式言語文およびその行番号から構成される除外反例を作成する。さらに除外反例作成部１１０は、上記除外反例に対する編集をユーザから受け付けることで、上記除外反例を構成する形式言語文の任意の組合せによる別の除外反例を作成する。その際ユーザは、記号“＊”を用いることで、形式言語文の任意回数の繰り返しを記述することもできる。除外反例作成部１１０は作成した除外反例を、除外反例保持部１１１に登録する。
【００２０】
形式言語仕様記述更新部１１２は、除外反例保持部１１１に保持している除外反例を取得し、上記除外反例に基づいて形式言語仕様記述保持部１０３に保持している形式言語仕様記述を更新する。具体的には形式言語仕様記述更新部１１２は、上記除外反例を構成する形式言語文の実行を記録するためのトレース配列の定義と、上記形式言語文を実行した場合に上記トレース配列に上記形式言語文を表す定数を代入するトレース情報作成処理を、上記形式言語仕様記述に挿入する。
【００２１】
検証性質更新部１１３は、除外反例保持部１１１に保持している除外反例を取得し、上記形式言語仕様記述に挿入した上記トレース配列が、上記除外反例の示す順序で上記形式言語文を表す定数を保持しているかを判定するためのトレース判定式を作成する。そして検証性質更新部１１３は、検証性質保持部１０２に保持している検証性質記述を、「上記検証性質が成立しなければ、その実行系列においてトレース判定式が成立する」という性質の記述に置き換える。
【００２２】
図２は、図１に示した偽反例除外支援装置を実現するハードウェア構成の例を示す図である。偽反例除外支援装置２０１は一例として、パーソナルコンピュータ（ＰＣ）等の汎用的な計算機で、ＣＰＵ２０２、メモリ２０３、補助記憶装置２０４、表示装置２０５、入力装置２０６、及び外部媒体入出力装置２０７を備える。
【００２３】
ＣＰＵ２０２は、メモリ２０３に記憶されたプログラムを実行することによって、各種処理を実行する。メモリ２０３は、ＣＰＵ２０２のワークエリアとして機能し、プログラム及びプログラムの実行に必要なデータを記憶する。具体的にはメモリ２０３には、ＣＰＵ２０２に実行されることによって偽反例除外支援装置２０１を、編集部１０１、自然言語文挿入部１０４、検証部１０６、除外反例作成部１１０、形式言語仕様記述更新部１１２、及び検証性質更新部１１３、の機能ブロックを備えた装置として動作させるためのプログラム、及びこのプログラムの実行に必要なデータが記憶される。
【００２４】
なお、以下では、偽反例除外支援装置２０１で実行される各種処理の内容を説明する際、除外反例作成部１１０等の機能ブロックを処理の主体として説明することがある。先に述べたとおり、除外反例作成部１１０等は、プログラムがＣＰＵ２０２に実行されることによって実現されたものである。そのため以下の説明において、機能ブロックを主語にして記述されている処理は、実際にはＣＰＵ２０２がその処理を行うことを意味する。ただし説明が冗長になることを避けるため、本実施例では、機能ブロックを処理の主体として、各種処理の内容を説明する。
【００２５】
また、偽反例除外支援装置２０１で実行されるプログラム（偽反例除外支援装置２０１を、上で述べた各機能ブロックを有する装置として動作させるためのプログラム）は、プログラム配布サーバや記憶メディアを介して提供され、プログラムを実行する装置にインストールされてもよい。なお、ここでの記憶メディアとは、データを非一時的に記憶するコンピュータ可読媒体を意味し、例えばＩＣカード、ＳＤカード、ＤＶＤ等の不揮発性記憶媒体である。
【００２６】
補助記憶装置２０４は、各種データを格納する。補助記憶装置２０４は例えば、ハードディスク装置などの不揮発性記憶媒体を用いた記憶装置である。上で述べた、検証性質保持部１０２、形式言語仕様記述保持部１０３、言語間対応関係保持部１０５、反例保持部１０７、および除外反例保持部１１１は、補助記憶装置２０４の有する記憶領域により構成される。
【００２７】
そのため、本実施例の説明において、たとえば「反例保持部１０７に情報を格納する」という記述がある箇所は、実際には反例保持部１０７を構成する補助記憶装置２０４の記憶領域に情報が格納されることを意味する。また、検証性質保持部１０２、形式言語仕様記述保持部１０３、言語間対応関係保持部１０５、および除外反例保持部１１１について、上と同様な記述がなされている場合にも同様に、補助記憶装置２０４の記憶領域に情報が格納されることを意味する。
【００２８】
また別の実施形態として、検証性質保持部１０２、形式言語仕様記述保持部１０３、言語間対応関係保持部１０５、反例保持部１０７、および除外反例保持部１１１は、メモリ２０３の記憶領域を用いて構成されてもよい。
【００２９】
あるいは、編集部１０１、自然言語文挿入部１０４、検証部１０６、反例保持部１０７、除外反例作成部１１０、形式言語仕様記述更新部１１２、及び検証性質更新部１１３を構成するプログラムの少なくとも一部についても、補助記憶装置２０４に格納されても良い。その場合、各種処理実行の際には、ＣＰＵ２０２が補助記憶装置２０４に格納されたプログラムをメモリ２０３へ読み出して、プログラムを実行する。また各プログラムは、あらかじめ、メモリ２０３または補助記憶装置２０４に格納されていても良いし、必要に応じ、利用可能な媒体を介して、他の装置からメモリ２０３または補助記憶装置２０４に導入されてもよい。媒体とは、例えば、外部媒体入出力装置２０７に着脱可能な記憶媒体、または、ネットワークや、ネットワークを伝搬する搬送波やデジタル信号などの通信媒体を指す。
【００３０】
表示装置２０５は、プログラムの処理結果などを表示する。表示装置２０５は、例えば、ディスプレイなどである。入力装置２０６は、処理の実行指示及び処理に必要な情報の入力などを利用者から受け付ける。入力装置２０６は、例えば、キーボード及びマウスなどである。
【００３１】
外部媒体入出力装置２０７は、外部媒体に格納されているデータなどの入出力を行う。外部媒体は、外部媒体入出力装置２０７に着脱可能で可搬性のある記憶媒体であり、外部媒体入出力装置２０７は、外部媒体に読み書き可能なドライブ装置などである。なお、図２に示したハードウェア構成は一例であり、偽反例除外支援装置２０１は上で説明した以外の構成物を備えていてもよい。たとえば偽反例除外支援装置２０１はネットワークインタフェースを有し、ネットワークインタフェースを介して、外部機器から必要な情報を偽反例除外支援装置２０１に入力するように構成されていてもよい。また、偽反例除外支援装置２０１は必ずしも単一の計算機でなくてもよい。ネットワークで相互接続された複数台の計算機から、偽反例除外支援装置２０１が構成されていてもよい。
【００３２】
図３は、形式言語仕様記述とその検証性質記述の例である。本実施例の説明では一例として、形式言語仕様記述と検証性質記述が、公知の形式言語であるPromelaの構文規則に従って記述されている例を説明する。また本実施例では、検証ツールの一種であるSPINを用いて形式言語仕様記述の検証が行われる例を説明する。そのため本実施例では、形式言語仕様記述３０１及び検証性質記述３０２に記述されている、個々の内容の説明は略す。
【００３３】
形式言語仕様記述３０１は、編集部１０１により入力装置２０６および表示装置２０５を介して編集され、形式言語仕様記述保持部１０３に保持される。同様に検証性質記述３０２は、編集部１０１により入力装置２０６および表示装置２０５を介して編集され、検証性質保持部１０２に保持される。また別の実施形態として、形式言語仕様記述３０１と検証性質記述３０２のうち少なくとも一方が、外部媒体入出力装置２０７あるいはネットワークを介して偽反例除外支援装置２０１に入力され、形式言語仕様記述保持部１０３や検証性質保持部１０２に格納されてもよい。つまり、形式言語仕様記述３０１と検証性質記述３０２は必ずしも、偽反例除外支援装置２０１内で作成（編集）されたものでなくても良い。
【００３４】
図４は、言語間対応関係保持部１０５が保持する言語間対応関係の例である。
【００３５】
言語間対応関係４０１は、形式言語仕様記述の行番号４０２、形式言語文４０３、および自然言語文４０４を含む。形式言語文４０３を説明する自然言語記述として自然言語文４０４が定義されていることを示している。形式言語仕様記述において、同一の形式言語文が複数回現れる可能性があるため、形式言語仕様記述の行番号４０２にて形式言語文４０３を特定している。本実施例の説明においては、形式言語仕様記述内の同一行に、同一の形式言語文が複数回出現しない場合の例を説明する。ただし、同一の行に、同一の形式言語文が複数回現れる形式言語仕様記述が取り扱われる場合は、行頭からの文字数などを言語間対応関係４０１に追加することで、形式言語文４０３の示す形式言語文を一意に識別できるようになる。
【００３６】
図５は、自然言語文挿入部１０４が、自然言語文を反例に出力するように形式言語仕様記述３０１を更新した結果の例である。
【００３７】
記述５０１〜５０５は、それぞれ自然言語文を反例に出力するために、自然言語文挿入部１０４によって挿入された形式言語の記述である。例えば記述５０１は、形式言語文３０３（x = 3）に対応する自然言語文“初期化”を反例に出力するために挿入された記述である。また自然言語文“初期化”の前には、自然言語文の接頭辞として定義した文字列“TRACE”が挿入されている。この接頭辞は、実施例２で説明する自然言語反例作成部１０８が自然言語反例を作成する際に、反例から自然言語文を抽出するための文字列検索キーワードとして使用する。本実施例では接頭辞に“TRACE”が用いられる例を説明するが、別の文字列が使用されてもよい。また図５の例では、形式言語文３０３と記述５０１とがatomic節と呼ばれる節内に括られている。これにより、形式言語文３０３と記述５０１は必ず連続して実行されるため、反例においても形式言語文３０３と記述５０１は連続して現れる。
【００３８】
図６は、自然言語文挿入部１０４の手順例を示すフローチャートである。以下に示す処理は、偽反例除外支援装置２０１の備えるＣＰＵ２０２が、メモリ２０３で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。
【００３９】
自然言語文挿入部１０４は、形式言語仕様記述保持部１０３から形式言語仕様記述を取得し、画面に表示する。そして自然言語文挿入部１０４は、上記形式言語仕様記述を構成する文に対するユーザからの選択入力を受け付ける（ステップ６０１）
【００４０】
続いて自然言語文挿入部１０４は、ステップ６０１にて選択された形式言語文を説明する自然言語文の入力をユーザから受け付ける（ステップ６０２）。
【００４１】
自然言語文挿入部１０４は、上記形式言語文の直後に、上記自然言語文を反例に出力するための記述を挿入する。さらに上記形式言語文と上記自然言語文をatomic節にて括り、挿入された記述内容を形式言語仕様記述保持部１０３内の形式言語仕様記述に反映する（ステップ６０３）。例えば、ステップ６０１にて形式言語文３０３が選択され、ステップ６０２ではその対応する自然言語文として“初期化”が入力されたとする。その場合、自然言語文挿入部１０４は、記述５０１を作成し、形式言語文３０３の直後に挿入する。さらに自然言語文挿入部１０４は、形式言語文３０３と記述５０１をatomic節にて括る。
【００４２】
自然言語文挿入部１０４は、上記形式言語文とその行番号、および上記自然言語文を、言語間対応関係として言語間対応関係保持部１０５に登録する（ステップ６０４）。例えばステップ６０３と同様に、ステップ６０１にて形式言語文３０３が選択され、ステップ６０２ではその対応する自然言語文として“初期化”が入力されたとする。その場合、自然言語文挿入部１０４は言語間対応関係４０１の1行目に示す情報を作成し、言語間対応関係保持部１０５に登録する。
【００４３】
図７は、自然言語文挿入部１０４における自然言語文挿入画面の例である。
【００４４】
自然言語文挿入画面１７０６は、形式言語仕様記述を表示する形式言語仕様記述表示部１７０１、形式言語仕様記述において選択中の行を表示する選択行表示部１７０２、選択中の行における形式言語文を表示する形式言語文表示部１７０３、自然言語文の入力を受け付ける自然言語文入力受付部１７０４、および上記自然言語文を反例に出力するための記述を、上記形式言語仕様記述に挿入するための挿入ボタン１７０５を含む。
【００４５】
形式言語仕様記述表示部１７０１において、ユーザから形式言語文の選択入力を受け付けると、自然言語文挿入部１０４は選択された行の番号と、その行における形式言語文を、それぞれ選択行表示部１７０２および形式言語文表示部１７０３に表示する（ステップ６０１）。そして自然言語文挿入部１０４は、自然言語文入力受付部１７０４にて自然言語文の入力を受け付ける（ステップ６０２）。その後ユーザが挿入ボタン１７０５を押下すると、自然言語文挿入部１０４は上記選択された行に、上記自然言語文を反例に出力するための記述を挿入し、さらに言語間対応関係４０１に記録すべき情報を作成して、言語間対応関係保持部１０５に格納する（ステップ６０３，６０４）。
【００４６】
ユーザは上記の手順を任意回繰り返すことで、形式言語仕様記述を構成する任意の形式言語文に対して、その意味を説明する自然言語文を反例に出力するようにする。その後ユーザは、自然言語文の挿入された形式言語仕様記述（及び検証性質記述）を検証部１０６に与え、検証部１０６に検証を実行させる。
【００４７】
図８は、自然言語文挿入部１０４によって自然言語文が挿入された形式言語仕様記述について検証部１０６が検証を行った結果、検証部１０６によって出力される反例（検証性質を満たさない場合の、形式言語仕様記述の実行系列）の例である。なお検証部１０６は、出力した反例を反例保持部１０７に格納する。
【００４８】
反例を構成する文の読み方を説明する。反例を構成する文は、実行系列におけるステップ番号、プロセスIDおよびプロセス名、形式言語仕様記述を保存したファイル名、形式言語仕様記述における行番号、および形式言語文にて構成される。例えば、図８の１行目は、1:proc 0 (p1) file:4 [x = 3]と記述されている。これは、ファイル名“file”の“4”行目に記載された“x = 3”という形式言語文７０１を、実行系列の第“１”ステップ目に実行したことを意味する。さらに上記“x = 3”という処理は、“proc 0 (p1)”というプロセスの処理であることを意味する。反例に含まれる形式言語文７０１〜７０６、および自然言語文７０７〜７１２は、後の説明にて参照する。
【００４９】
続いて除外反例の作成処理について説明する。図９は、除外反例作成部１１０が作成する除外反例の例である。
【００５０】
除外反例８０１は少なくとも、形式言語文８０３と、形式言語仕様記述におけるその形式言語文８０３の行番号８０２の組を１以上含む。本実施例では、形式言語文８０３と、その形式言語文８０３の形式言語仕様記述内における行番号８０２の組を、「除外反例文」と呼ぶ。なお、除外反例文は行番号以外の情報を含んでいてもよい。少なくとも除外反例文の形式言語文が、形式言語仕様記述内のどこに存在する文であるか、特定可能な情報が除外反例文に含まれていればよい。たとえば行番号の代わりに、形式言語仕様記述の先頭からのバイトオフセットが、除外反例文に含まれていてもよい。また除外反例文に、形式言語文と行番号以外の情報が含まれていてもよい。
【００５１】
除外反例作成部１１０は、除外反例に対する編集入力をユーザから受け付けることで、上記除外反例を構成する形式言語文の任意の組合せによる別の除外反例を作成する。除外反例８０４は、除外反例８０１を編集することで作成された除外反例の例である。同様に除外反例８０５は、除外反例８０４を編集することで作成された除外反例の例である。記号８０６は、形式言語文“x--”の任意回数の繰り返しを意味する。これらの除外反例は、除外反例保持部１１１に格納される。
【００５２】
図１０は、除外反例作成部１１０の手順例を示すフローチャートである。以下に示す処理は、偽反例除外支援装置２０１の備えるＣＰＵ２０２が、メモリ２０３で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。
【００５３】
除外反例作成部１１０は、反例保持部１０７から反例を取得し、上記反例を構成する形式言語文の選択をユーザから受け付ける（ステップ９０１）。例えば、図８に示す反例の例では、形式言語文７０１〜７０６などを選択できる。
【００５４】
除外反例作成部１１０は、上記反例から、ステップ９０１にて選択された形式言語文の形式言語仕様記述における行番号を取得する。そして、少なくとも上記行番号と上記形式言語文を含む除外反例を作成する（ステップ９０２）。例えば、ステップ９０１にて形式言語文７０１〜７０６を選択した場合、除外反例８０１を作成する。
【００５５】
除外反例作成部１１０は、ステップ９０２で作成した除外反例に対する編集をユーザから受け付けることで、上記除外反例を構成する形式言語文（除外反例文）の任意の組合せによる別の除外反例を作成する。その際ユーザは、記号“＊”を用いることで、形式言語文の任意回数の繰り返しを記述することもできる（ステップ９０３）。例えば、除外反例作成部１１０はユーザからの入力に従って除外反例８０１を編集することで、除外反例８０４を作成できる。同様に除外反例作成部１１０はユーザからの入力に従って除外反例８０４を編集することで、除外反例８０５を作成できる。
【００５６】
除外反例作成部１１０は、ステップ９０２にて作成した除外反例、あるいはステップ９０３にて作成した除外反例を、除外反例保持部１１１に登録する（ステップ９０４）。
【００５７】
図１１は、除外反例作成部１１０における除外反例作成画面の例である。
【００５８】
除外反例作成画面１８０９は、反例を表示する反例表示部１８０１、反例において選択中の行における形式言語文を表示する形式言語文表示部１８０３、上記選択された形式言語文の、形式言語仕様記述における行番号を表示する行番号表示部１８０２、選択した形式言語文を除外反例表示部１８０５の最後尾に追加する追加ボタン１８０４、除外反例を表示する除外反例表示部１８０５、繰り返しを意味する記号“＊”を入力する記号入力部１８０８、除外反例表示部１８０５において選択された形式言語文を削除する削除ボタン１８０６、および除外反例表示部１８０５において選択された形式言語文を複製して除外反例表示部１８０５の最後尾に追加する複製ボタン１８０７、除外反例を除外反例保持部１１１に記録する登録ボタン１８１０を含む。
【００５９】
反例表示部１８０１において、形式言語文の選択入力を受け付けると（ステップ９０１）、除外反例作成部１１０は、選択された形式言語文と、その形式言語文の形式言語仕様記述における行番号を、それぞれ形式言語文表示部１８０３および行番号表示部１８０２に表示する。図１１の反例表示部１８０１の例では、選択中の行は下線が引かれた状態で表示されている。そして、追加ボタン１８０４の押下を受け付けると、除外反例作成部１１０は選択された形式言語文を除外反例表示部１８０５の最後尾に追加する（ステップ９０２）。
【００６０】
除外反例表示部１８０５では、ユーザは形式言語文の追加、削除、あるいは形式言語文の順序の入れ替えなどの編集作業が可能である（ステップ９０３）。ユーザは除外反例表示部１８０５上でドラッグ＆ドロップ等の作業を行って形式言語文を移動することで、形式言語文の順序を変更できる。さらに記号入力部１８０８を利用することで、ユーザは記号“＊”を入力できる。また除外反例表示部１８０５において、ユーザが形式言語文の１つを選択した後に削除ボタン１８０６を押下すると、除外反例作成部１１０は選択中の形式言語文を除外反例表示部１８０５から削除する。同様に、ユーザが除外反例表示部１８０５において形式言語文を選択した後に複製ボタン１８０７を押下すると、除外反例作成部１１０は選択中の上記形式言語文を複製し、除外反例表示部１８０５の最後尾に追加する。
【００６１】
また、登録ボタン１８１０が押下されると、除外反例作成部１１０は除外反例表示部１８０５に表示されている除外反例の内容を、除外反例保持部１１１に登録する（ステップ９０４）。
【００６２】
なお、本実施例では、除外反例作成部１１０は検証部１０６で出力された反例に対する編集入力をユーザから受け付けることで、除外反例を作成する例を説明している。つまり本実施例では、除外反例を作成する前に少なくとも１回は、検証部１０６による検証を行う例を説明している。ただし別の実施形態として、検証部１０６で出力された反例を用いずに除外反例が作成されてもよい。たとえばユーザが編集部１０１を用いて、（検証部１０６で出力された反例を用いずに）図９に示されるような除外反例を作成し、除外反例保持部１１１に格納してもよい。この場合、偽反例除外支援装置２０１は、除外反例の作成前に検証部１０６による検証を行って反例を出力する必要はない。またこの場合、除外反例作成部１１０は、上で説明した機能を必ずしも有している必要はない。ユーザからのデータ入力を受け付けて、ユーザから入力された内容（除外反例）を除外反例保持部１１１に格納する機能（つまり編集部１０１と同程度の機能）を有していればよい。さらに別の実施形態として、偽反例除外支援装置２０１が除外反例作成部１１０を有さず、外部の計算機で作成された除外反例を、例えばネットワークを介して受信して、除外反例保持部１１１に格納するように構成されていてもよい。
【００６３】
続いて、形式言語仕様記述更新部１１２の行う処理について説明する。除外反例が除外反例保持部１１１に登録されると、形式言語仕様記述更新部１１２の実行が可能になる。偽反例除外支援装置２０１は除外反例が除外反例保持部１１１に登録されたことを契機に、形式言語仕様記述更新部１１２の実行を開始しても良い。あるいは別の実施形態として、偽反例除外支援装置２０１は、ユーザから形式言語仕様記述更新部１１２による処理の開始の指示を受領したことを契機に、形式言語仕様記述更新部１１２の実行を開始するように構成されていてもよい。
【００６４】
図１２は、除外反例８０４に基づき、形式言語仕様記述更新部１１２が更新した形式言語仕様記述の例である。
【００６５】
形式言語仕様記述更新部１１２は、除外反例８０４に基づき、図５に示す形式言語仕様記述に対して、除外反例に含まれる形式言語文を表す定数の定義１３０１、トレース配列の定義１３０２、およびトレース情報作成処理１３０３、１３０４を挿入する。本実施例では、形式言語仕様記述更新部１１２によって挿入される、定数の定義１３０１、トレース配列の定義１３０２、トレース情報作成処理１３０３のセットを、トレース挿入用記述と呼ぶ。
【００６６】
定数の定義１３０１には、DecとFinの２つの定数が定義されている。除外反例８０４には、２種類の除外反例文(“7:  x-”と“16: x--”)が定義されているので、形式言語仕様記述更新部１１２は定数の定義１３０１に２つの定数を定義する。なお、Decは7行目の形式言語文“x--”を表し、同様にFinは16行目の形式言語文“x--”を表す。形式言語仕様記述更新部１１２はこれら定数の名前に、重複のない任意の名前を設定する。
【００６７】
トレース配列の定義１３０２では、上記形式言語文の実行を記録するためのトレース配列を表す変数trと、その配列インデックスを保持する変数indexが宣言されている。上記トレース配列の長さは、除外反例の行数よりも大きく設定する必要がある。本実施例では１００としているが、除外反例の行数よりも大きければ任意の値で構わない。
【００６８】
トレース情報作成処理１３０３、１３０４では、上記形式言語文の実行と同時に、定数の定義１３０１にて定義した、上記形式言語文を表す定数を代入している。例えばトレース情報作成処理１３０３では、トレース配列trに対して7行目の形式言語文“x--”を表す定数Decを代入している。そして、作成したトレース情報作成処理１３０３と、7行目の形式言語文“x--”はatomic節にて括られているので、図１２の形式言語仕様記述が検証部１０６で実行されると、7行目の形式言語文“x--”の実行と同時に、トレース配列trにその実行を表す定数Decが格納される。
【００６９】
このように形式言語仕様記述更新部１１２によって、トレース挿入用記述が形式言語仕様記述に挿入されるため、形式言語仕様記述の検証が行われると（検証言語仕様記述が検証部１０６によって検証されると）、除外反例に含まれる形式言語文が実行される毎に、トレース配列に、実行された形式言語文を表す定数が実行順に格納される。そのため、形式言語仕様記述の検証後に（あるいは検証中に）、トレース配列を参照すると、形式言語仕様記述に含まれる各形式言語文が、除外反例に記述されている順に実行されたか否かを判断することができる。
【００７０】
図１３は、形式言語仕様記述更新部１１２の手順例を示すフローチャートである。以下に示す処理は、偽反例除外支援装置２０１の備えるＣＰＵ２０２が、メモリ２０３で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。
【００７１】
形式言語仕様記述更新部１１２は、除外反例保持部１１１から除外反例を読み出す。そして形式言語仕様記述更新部１１２は、読み出された除外反例の中から、除外反例文を重複を排除して抽出する。さらに形式言語仕様記述更新部１１２は、抽出した除外反例文ごとに、その除外反例文を表す定数を決定し、決定した定数の定義を、形式言語仕様記述保持部１０３に格納されている形式言語仕様記述に書き加える（ステップ１４０１）。ここで決定される定数の数は、抽出された除外反例文の数と同じである。
【００７２】
例えば除外反例８０４には、４行の除外反例文が記述されている。その中から重複のないように除外反例文を抽出する場合、7行目の形式言語文（7:   x--）と、16行目の形式言語文（16:   x--）の2つの形式言語文が抽出される（つまり、形式言語文の内容が同一（x--）でも行番号が異なる２つの行（除外反例文）が除外反例に含まれている場合、形式言語仕様記述更新部１１２は２つの除外反例文は異なる文と判断して、２つの除外反例文を抽出する）。そのため、図１２における定数の定義１３０１では、DecとFinの2つの定数が定義されている。Decは7行目の形式言語文に、Finは16行目の形式言語文にそれぞれ対応する。定数の名称及び値は、形式言語仕様記述更新部１１２が任意に決定できる。
【００７３】
また、ある除外反例文に対して“＊”を付与した除外反例文と、“＊”を付与していない除外反例文の両方が除外反例に含まれる場合、それらの除外反例文は別の文として扱われる。例えば形式言語仕様記述更新部１１２が除外反例８０５から除外反例文を抽出する場合、記号８０６が付与された除外反例文“（x--）＊”を“（x--）”とは別の文として扱う。そのためこの場合には、形式言語仕様記述更新部１１２はFinとDecに加えて、“（x--）＊”に対応する別の定数（例えばDec_itr）を定義する。
【００７４】
形式言語仕様記述更新部１１２は、上記除外反例を構成する除外反例文の実行をトレース情報として記録するため、形式言語仕様記述保持部１０３内の形式言語仕様記述に、ステップ１４０１で定義した定数を格納可能なトレース配列とその配列インデックスを保持する変数の定義を書き加える（ステップ１４０２）。例えば図１２におけるトレース配列の定義１３０２では、トレース配列trとそのインデックスを保持する変数indexを定義している。
【００７５】
形式言語仕様記述更新部１１２は、ステップ１４０１で抽出された除外反例文のうち、まだステップ１４０４の処理が行われていない除外反例文を１つ選択する（ステップ１４０３）。
【００７６】
形式言語仕様記述更新部１１２は、ステップ１４０３で選択した除外反例文について、上記配列インデックスを更新する（１を加算する）処理“index++”と、選択された除外反例文を表す定数をトレース配列に代入するトレース情報作成処理を、形式言語仕様記述保持部１０３内の形式言語仕様記述における上記形式言語文と同一のatomic節内に記述する（ステップ１４０４）。例えば、除外反例８０４に含まれる形式言語文のうち、形式言語仕様記述の7行目に位置する“x--”についてトレース情報作成処理を挿入した結果が、図１２におけるトレース情報作成処理１３０３である。
【００７７】
また、ステップ１４０３で選択した除外反例文が“＊”付きの除外反例文の場合、形式言語仕様記述に挿入されるトレース情報作成処理は、“＊”なしの場合とは異なる。その場合のトレース情報作成処理は、「配列インデックスの示すトレース配列に“＊”なしの上記除外反例文に対応する定数が格納されている場合は、上記トレース配列に“＊”付きの上記除外反例文に対応する定数を代入する。あるいは、配列インデックスの示すトレース配列に“＊”付きの上記除外反例文に対応する定数が格納されている場合は、上記トレース配列は更新しない。上記以外の場合は、配列インデックスを“index++”にて更新した後に、“＊”なしの上記除外反例文に対応する定数を上記トレース配列に代入する」という処理を表す。例えば、記号８０６が付与された除外反例文に対応する定数をDec_itrとすると、記号８０６が付与された除外反例文に対応するトレース情報作成処理は、“if :: tr[index] == Dec -> tr[index] = Dec_itr; :: tr[index] == Dec_itr -> skip; :: else -> index++; tr[index] = Dec;fi”となる。
【００７８】
形式言語仕様記述更新部１１２は、ステップ１４０１で抽出された全ての除外反例文についてステップ１４０４の処理を実行したかチェックする。全ての除外反例文についてステップ１４０４を実行済みの場合、形式言語仕様記述更新部１１２は処理を終了し、次に検証性質更新部１１３の処理を開始する。未取得の除外反例文がある場合は、形式言語仕様記述更新部１１２は再びステップ１４０３から処理を実行する（ステップ１４０５）。
【００７９】
続いて、検証性質更新部１１３の行う処理について説明する。図１４は、検証性質更新部１１３が除外反例８０４に基づき、検証性質記述３０２（図３）を更新した時の、更新後の検証性質記述の例である。
【００８０】
検証性質更新部１１３は、上記トレース配列が上記除外反例の示す順序で上記除外反例文を表す定数を保持しているかを判定するためのトレース判定式を作成する。除外反例８０４に基づいて作成されたトレース判定式が、トレース判定式１５０２である。そして検証性質更新部１１３は、作成されたトレース判定式１５０２を用いて、検証性質記述３０２を、「上記検証性質が成立しなければ、その実行系列においてトレース判定式が成立する」という性質の記述に書き換える。検証性質記述１５０１は、検証性質更新部１１３によって検証性質記述３０２が書き換えられた後の状態である。このように検証性質記述が書き換えられるため、検証部１０６による検証の結果（あるいは検証の過程で）、（書き換え前の）検証性質が成立しなかった場合であっても、もしも除外反例に記述されている順に形式言語仕様記述を構成する形式言語文が実行されていた場合、検証部１０６は反例（除外反例）の出力を行わない。
【００８１】
図１５は、検証性質更新部１１３の手順例を示すフローチャートである。以下に示す処理は、偽反例除外支援装置２０１の備えるＣＰＵ２０２が、メモリ２０３で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。
【００８２】
検証性質更新部１１３は、検証性質保持部１０２から更新前の検証性質を読み出し、一旦メモリ２０３等に記憶する（ステップ１６０１）。例えば、検証性質記述３０２の場合、検証性質更新部１１３は“[](!(x < 0))”を記憶する。
【００８３】
検証性質更新部１１３は、除外反例に含まれる除外反例文を表す定数とその格納のためのトレース配列を、形式言語仕様記述保持部１０３から取得する（ステップ１６０２）。例えば除外反例８０４の場合は、定数の定義１３０１に定義されているDecやFin等の定数と、トレース配列の定義１３０２に定義されているトレース配列trを取得する。なお、別の実施形態として検証性質更新部１１３は、除外反例に含まれる形式言語文を表す定数とその格納のためのトレース配列を、形式言語仕様記述更新部１１２から受領してもよい。
【００８４】
検証性質更新部１１３は、上記トレース配列が、上記除外反例の示す順に上記定数を保持しているかを判定するためのトレース判定式を作成する（ステップ１６０３）。例えば除外反例８０４の場合は、トレース判定式１５０２を作成する。
【００８５】
検証性質更新部１１３は、更新前の検証性質が成立しなければその実行系列においてトレース判定式が成立するという意味の式を作成し、更新後の検証性質として検証性質保持部に登録する（ステップ１６０４）。例えば除外反例８０４の場合は、トレース判定式１５０２を用いて検証性質記述１５０１を作成し、検証性質保持部１０２に格納されている検証性質を、今回作成した検証性質記述１５０１に書き換える。
【００８６】
この後ユーザは、更新された形式言語仕様記述と検証性質記述を用いて、検証部１０６による検証を行うと良い。更新された形式言語仕様記述と検証性質記述を用いて検証が行われた場合、検証部１０６は除外反例を出力しない。またユーザは、検証部１０６を用いて検証を行う代わりに、偽反例除外支援装置２０１以外の計算機にインストールされている検証ツールに、更新された形式言語仕様記述と検証性質記述を与えることで、検証を行ってもよい。
【００８７】
以上が、本発明の実施例１に係る偽反例除外支援装置の説明である。本発明の実施例１に係る偽反例除外支援装置は、形式言語で記述した仕様記述である形式言語仕様記述が、その仕様が満たすべき性質を記述した検証性質記述を満たすか検証された結果出力される１以上の反例の中から、除外すべき除外反例を登録するための入力を受け付ける。そして偽反例除外支援装置は、形式言語文の実行を記録するためのトレース配列の定義と、上記形式言語文を実行した場合に上記トレース配列に上記形式言語文を表す定数を代入するトレース情報作成処理を上記形式言語仕様記述に挿入する。また偽反例除外支援装置は、上記トレース配列を使用して、トレース配列が上記除外反例の示す順序で上記形式言語文を表す定数を保持しているかを判定するためのトレース判定式を作成し、上記検証性質記述を、「上記検証性質が成立しなければ、その実行系列においてトレース判定式が成立する」という性質の記述に置き換える。これにより、更新後の形式言語仕様記述が、同じく更新後の検証性質記述を満たすかを検証した場合、上記除外反例が検証の結果として出力されることを防止できるようになる。よって本実施例に係る偽反例除外支援装置によれば、人手で形式言語仕様記述を詳細化することなく、一度偽反例と判定した反例を検証の出力から除外できるようになるため、システム仕様の不具合検出にかかる作業時間および作業工数を削減できる。
【００８８】
また本実施例に係る偽反例除外支援装置は、上記形式言語仕様記述が上記検証性質記述を満たすか検証した結果出力される反例を編集することで、除外反例を作成することもできるため、何もない状態から除外反例を作成するよりも効率よく除外反例を作成することができる。また本実施例に係る偽反例除外支援装置は、出力された反例を編集することで、任意の別の除外反例を作成することもできる。その際、記号“＊”を用いることで、形式言語文の任意回数の繰り返しを記述することもできる。これにより、検証結果として出力された反例だけでなく、出力された反例から連想される別の反例も、偽反例として検証出力から除外できるようになるため、システム仕様の不具合検出にかかる作業時間および作業工数を削減できる。
【実施例２】
【００８９】
続いて実施例２に係る偽反例除外支援装置の説明を行う。実施例２に係る偽反例除外支援装置のハードウェア構成は、実施例１で説明したもの（図２）と同じであるので、ここでの説明は略す。
【００９０】
図１６に、実施例２に係る偽反例除外支援装置の有する機能ブロックを示す。これらの機能ブロックの多くは実施例１で説明したものと同じであるため、以下では主に、実施例１にはない機能ブロックについて説明する。
【００９１】
実施例２に係る偽反例除外支援装置は、実施例１で説明した除外反例作成部１１０に代えて、自然言語反例作成部１０８、自然言語反例向け除外反例作成部１１４を有する。また実施例２に係る偽反例除外支援装置は、実施例１で説明した各記憶部に加えて、自然言語反例保持部１０９という記憶部を有する。その他の点は、実施例１で説明したものと同じである。
【００９２】
自然言語反例作成部１０８は、反例保持部１０７に保持している反例を取得し、上記反例に含まれる自然言語文を抽出することで自然言語反例を作成する。作成した上記自然言語反例は、自然言語反例保持部１０９に登録する。
【００９３】
自然言語反例向け除外反例作成部１１４は、自然言語反例保持部１０９に保持している自然言語反例を取得し、上記自然言語反例を構成する自然言語文の選択および編集をユーザから受け付けることで、上記自然言語反例を構成する自然言語文の任意の組合せにて表される別の自然言語反例を作成する。その際ユーザは、記号“＊”を用いることで、自然言語文の任意回数の繰り返しを記述することもできる。また自然言語反例向け除外反例作成部１１４は、上記自然言語反例を構成する各自然言語文を、対応する形式言語文に置き換えることで、形式言語の除外反例に変換できる。この変換は、言語間対応関係保持部１０５に保持している形式言語文と自然言語文との対応関係に基づいて行われる。この変換によって作成された除外反例は、除外反例保持部１１１に登録される。
【００９４】
図１７は、自然言語反例作成部１０８が作成する自然言語反例の例である。
【００９５】
自然言語反例１００１は、図８に示す反例から、自然言語文７０７〜７１２を抽出することで作成した自然言語反例である。自然言語反例は、少なくとも自然言語文１００３と、その自然言語文に対応する形式言語文の形式言語仕様記述における行番号１００２を含む。また自然言語反例向け除外反例作成部１１４は、自然言語反例に対する編集をユーザから受け付けることで、自然言語反例を構成する自然言語文の任意の組合せによる別の自然言語反例を作成する。自然言語反例１００４は、自然言語反例１００１を編集することで作成された自然言語反例の例である。同様に自然言語反例１００５は、自然言語反例１００４を編集することで作成された自然言語反例の例である。記号１００６は、除外反例８０６における記号８０６と同様に、自然言語文“減算”の任意回数の繰り返しを意味する。これらの自然言語反例は、自然言語反例保持部１０９に保持される。
【００９６】
また、自然言語反例１００１は、自然言語反例向け除外反例作成部１１４によって、形式言語の除外反例８０１に変換される。同様に、自然言語反例１００４および自然言語反例１００５は、自然言語反例向け除外反例作成部１１４によって、それぞれ除外反例８０４および８０５に変換される。
【００９７】
図１８は、自然言語反例作成部１０８の手順例を示すフローチャートである。以下に示す処理は、偽反例除外支援装置２０１の備えるＣＰＵ２０２が、メモリ２０３で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。
【００９８】
自然言語反例作成部１０８は、反例保持部１０７から反例を取得し、上記反例に含まれる自然言語文を抽出する。抽出のためには、自然言語反例作成部１０８は反例の先頭から文字列検索を実行し、自然言語文の接頭辞として定義した“TRACE”を含む行を取得する。その際自然言語反例作成部１０８は、形式言語仕様記述において上記自然言語文を出力している記述の行番号も併せて取得する。本実施例では形式言語仕様記述において、自然言語文を出力する記述をその対応する形式言語文と同じ行に挿入しているため、上記行番号は、自然言語文に対応する形式言語文の行番号と一致する。自然言語反例作成部１０８は上記自然言語文と上記行番号を用いて、自然言語反例を作成する（ステップ１１０１）。例えば自然言語反例作成部１０８は、図８に示す反例から、“TRACE”を含む行（自然言語文７０７〜７１２）を抽出することで自然言語反例１００１を作成する。
【００９９】
そして自然言語反例作成部１０８は、ステップ１１０１にて作成した自然言語反例を、自然言語反例保持部１０９に登録し（ステップ１１０３）、処理を終了する。
【０１００】
図１９は、自然言語反例向け除外反例作成部１１４の手順例を示すフローチャートである。以下に示す処理は、偽反例除外支援装置２０１の備えるＣＰＵ２０２が、メモリ２０３で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。
【０１０１】
自然言語反例向け除外反例作成部１１４は、自然言語反例保持部１０９から自然言語反例を取得し、取得した自然言語反例に対する編集入力をユーザから受け付けることで、別の自然言語反例を作成する。その際ユーザは記号“＊”を用いることで、自然言語文の任意回数の繰り返しを記述する事もできる（ステップ１２０１）。
【０１０２】
自然言語反例向け除外反例作成部１１４は、言語間対応関係保持部１０５の保持する言語間対応関係４０１を参照することで、上記自然言語反例の自然言語文を、対応する形式言語文に置き換える。これにより上記自然言語反例が、形式言語の除外反例に変換される（ステップ１２０２）。
【０１０３】
ステップ１２０２の後、自然言語反例向け除外反例作成部１１４は、作成した除外反例を除外反例保持部１１１に登録する（ステップ１２０３）。
【０１０４】
図２０は、自然言語反例向け除外反例作成部１１４における自然言語反例の編集画面の例である。
【０１０５】
自然言語反例編集画面１９０５は、自然言語反例を表示する自然言語反例表示部１９０１、記号“＊”を入力する記号入力部１９０４、自然言語反例表示部１９０１において選択された自然言語文を削除する削除ボタン１９０２、自然言語反例表示部１９０１において選択された自然言語文を複製する複製ボタン１９０３、そして編集された自然言語反例を除外反例に変換して除外反例保持部１１１に記録する登録ボタン１８１０を含む。
【０１０６】
自然言語反例表示部１９０１では、ユーザはドラッグ＆ドロップ等にて自然言語文を移動することで、自然言語文の順序を変更できる。さらにユーザは記号入力部１８０８を利用することで、繰り返しを意味する記号“＊”を入力できる。また自然言語反例向け除外反例作成部１１４は、自然言語反例表示部１９０１において自然言語文の選択を受け付けた後に削除ボタン１９０２の押下を受け付けると、選択中の上記自然言語文を自然言語反例表示部１９０１から削除する。同様に自然言語反例向け除外反例作成部１１４は、自然言語反例表示部１９０１において自然言語文の選択を受け付けた後に複製ボタン１９０３の押下を受け付けると、選択中の上記自然言語文を複製し、自然言語反例表示部１９０１の最後尾に追加する。また、登録ボタン１９００が押下されると、自然言語反例向け除外反例作成部１１４は自然言語反例表示部１９０１に表示されている自然言語反例を、形式言語の除外反例に変換し、変換された除外反例を除外反例保持部１１１に登録する（ステップ１２０２、１２０３）。
【０１０７】
除外反例が作成された後の処理は、実施例１で説明したものと同様である。つまりユーザは、形式言語仕様記述更新部１１２を実行することで、形式言語仕様記述を更新し、さらに検証性質更新部１１３を実行することで検証性質記述の書き換えを行うとよい。そしてユーザは、更新された形式言語仕様記述と検証性質記述を用いて、検証部１０６による検証を行うとよい。
【０１０８】
以上が実施例２に係る偽反例除外支援装置の説明である。実施例２に係る偽反例除外支援装置は実施例１に係る偽反例除外支援装置と同様に、人手で形式言語仕様記述を詳細化することなく、容易に偽反例を検証出力から除外できるという特徴を有する。
【０１０９】
また実施例２に係る偽反例除外支援装置は、上記形式言語仕様記述を構成する任意の形式言語文に対して、その文の意味を説明する自然言語文の入力を受け付ける。そして、上記形式言語文の実行時に上記自然言語文を出力するように上記形式言語仕様記述を更新する。これにより、上記自然言語文が反例に追加されるため、上記反例から上記自然言語文のみを抽出することで、自然言語で記述された自然言語反例を作成できる。
【０１１０】
さらに実施例１で説明した偽反例除外支援装置が、出力された反例を編集して別の除外反例を作成することができるのと同様に、実施例２に係る偽反例除外支援装置は、自然言語反例に対する編集を受け付けることで、別の自然言語反例を作成することもできる。その際、形式言語の反例と同様に、記号“＊”を用いることで、自然言語文の任意回数の繰り返しを記述することもできる。これらの自然言語反例は、その構成要素である自然言語文を対応する形式言語文に置き換えることで、形式言語の除外反例に変換できる。そして上記除外反例に基づいて上記トレース配列の定義やトレース情報作成処理を挿入し、上記形式言語仕様記述を更新することができる。同様に、トレース判定式を作成し、検証性質記述を更新することもできる。これにより、形式言語ではなく自然言語上で除外反例を作成できるようになるため、形式言語を解読できない検証者でも、本発明による偽反例の除外を実施できるようになる。
【０１１１】
以上、本発明の実施例を説明してきたが、これらは、本発明の説明のための例示であって、本発明の範囲をこれらの実施例にのみ限定する趣旨ではない。本発明は、他の種々の形態でも実施する事が可能である。
【０１１２】
たとえば上で述べた実施例では、除外反例作成部等の機能ブロックが、汎用的な計算機のプロセッサでプログラムが実行されることにより実現される機能ブロックである例を説明した。ただし別の実施形態として、偽反例除外支援装置の一部または全ての機能ブロックは、ＦＰＧＡやＡＳＩＣ等のハードウェアで実装されていてもよい。
【０１１３】
また、上で述べた実施例では、除外反例を構成する形式言語文の実行を記録するために、トレース配列を定義して、除外反例を構成する形式言語文が実行される時にトレース配列にその旨を記録する処理（トレース情報作成処理）が、形式言語仕様記述に挿入された。ただし、トレース情報を記録するための方法は、これに限定されない。除外反例に記述された順序で除外反例を構成する形式言語文が実行された場合にその事実を（計算機のメモリ等に）記録するための処理を、計算機に行わせるための記述であれば、任意の形式の記述が形式言語仕様記述に挿入されてよい。
【０１１４】
また、実施例１では、偽反例除外支援装置が自然言語文挿入部１０４と言語間対応関係保持部１０５を有している例を説明したが、実施例１に係る偽反例除外支援装置は必ずしも、自然言語文挿入部１０４と言語間対応関係保持部１０５を有していなくてもよい。
【０１１５】
また、実施例１では除外反例作成部１１０を有する偽反例除外支援装置について説明し、実施例２では除外反例作成部１１０に代えて自然言語反例作成部１０８及び自然言語反例向け除外反例作成部１１４を備える偽反例除外支援装置について説明した。ただし別の実施形態として、偽反例除外支援装置が、自然言語反例作成部１０８及び自然言語反例向け除外反例作成部１１４と、除外反例作成部１１０の両方を備える構成もあり得る。
【０１１６】
この場合、偽反例除外支援装置はユーザに、形式言語文で記述された除外反例を作成するか、あるいは自然言語で記述された除外反例を作成するか、選択させるとよい。ユーザが形式言語文で記述された除外反例を作成することを選択した場合、偽反例除外支援装置は実施例１で説明した処理を行うことで形式言語仕様記述と検証性質記述の書き換えを行うとよい。そしてユーザが自然言語文で記述された除外反例を作成することを選択した場合、偽反例除外支援装置は実施例２で説明したように、自然言語反例向け除外反例作成部１１４によって除外反例を生成し、それを用いて形式言語仕様記述と検証性質記述の書き換絵を行うとよい。
【符号の説明】
【０１１７】
１０１：編集部、１０２：検証性質保持部、１０３：形式言語仕様記述保持部、１０４：自然言語文挿入部、１０５：言語間対応関係保持部、１０６：検証部、１０７：反例保持部、１０８：自然言語反例作成部、１０９：自然言語反例保持部、１１０：除外反例作成部、１１１：除外反例保持部、１１２：形式言語仕様記述更新部、１１３：検証性質更新部、１１４：自然言語反例向け除外反例作成部
【図１】
0006556091.tif 000002
【図２】
0006556091.tif 000003
【図３】
0006556091.tif 000004
【図４】
0006556091.tif 000005
【図５】
0006556091.tif 000006
【図６】
0006556091.tif 000007
【図７】
0006556091.tif 000008
【図８】
0006556091.tif 000009
【図９】
0006556091.tif 000010
【図１０】
0006556091.tif 000011
【図１１】
0006556091.tif 000012
【図１２】
0006556091.tif 000013
【図１３】
0006556091.tif 000014
【図１４】
0006556091.tif 000015
【図１５】
0006556091.tif 000016
【図１６】
0006556091.tif 000017
【図１７】
0006556091.tif 000018
【図１８】
0006556091.tif 000019
【図１９】
0006556091.tif 000020
【図２０】
0006556091.tif 000021