(57)【要約】      （修正有）【課題】プログラムの事後条件が事前に与えられた場合に当該プログラムの事前条件を効率よく近似的に生成することを可能とした事前条件生成装置およびその方法を提供する。【解決手段】事前条件生成装置は、プログラムを記憶するプログラム記憶部１５と、前記プログラムの事後条件を記憶する事後条件記憶部と、１つ以上の論理式の集合である必須条件を複数記憶する必須条件記憶部と、複数の論理式を記憶する論理式集合記憶部と、前記論理式集合記憶部から選択した１つ以上の前記論理式の集合である候補条件を前記必須条件と共通要素を持つように生成する候補条件生成部１０と、前記候補条件の論理積が成り立つときに前記プログラムが実行された直後に前記事後条件が成立するという命題が成立するか否かを判定する第１の判定部と、前記命題が成立すると決定された前記候補条件の論理積を、前記プログラムの事前条件として出力する出力部２１と、を備える。【選択図】図１
2010218148.tif 000002
【特許請求の範囲】
【請求項１】
命令型プログラミング言語によって記述されたプログラムを記憶するプログラム記憶部と、
１つ以上の論理式の論理積である、前記プログラムの事後条件を記憶する事後条件記憶部と、
前記事後条件が成立するために前記プログラムの実行直前において少なくともその要素の一つが満たされる必要のある、１つ以上の論理式の集合である必須条件を複数記憶する必須条件記憶部と、
複数の論理式を記憶する論理式集合記憶部と、
前記論理式集合記憶部から選択した１つ以上の前記論理式の論理積である候補条件を前記必須条件との共通要素を持つように生成する候補条件生成部と、
前記候補条件の論理積が成り立つときに前記プログラムが実行された直後に前記事後条件が成立するという命題が成立するか否かを、前記命題の反例が存在するか否かを検査することにより判定し、前記命題の反例が存在しないとき前記命題が成立し、前記命題の反例が存在するとき前記命題が成立しないことを決定する第１の判定部と、
前記命題が成立すると決定された前記候補条件の論理積を、前記プログラムの事前条件として出力する出力部と、
を備えた事前条件生成装置。
【請求項２】
前記論理式集合記憶部内の論理式を１つ以上組み合わせることにより部分集合Ｚを生成する部分集合生成部と、
前記論理式集合記憶部内の全論理式の集合Ｓから前記部分集合Ｚを除外した部分集合Ｓ−Ｚの論理積が成り立つときに前記プログラムが実行された直後に前記事後条件が成立するという命題が成立するか否かを前記命題の反例が存在するか否かを検査することにより判定する第２の判定部と、をさらに備え、
前記必須条件記憶部は、前記第２の判定部により前記命題が成立しないと判定された前記部分集合Ｚを前記必須条件として記憶する
ことを特徴とする請求項１に記載の事前条件生成装置。
【請求項３】
前記プログラムを一部に含む第２のプログラムを実行し、
前記第２のプログラムに含まれる変数の値の推移であるログを記録し、
前記ログに基づいて前記プログラムの実行直前および直後において成立する不変条件を生成し、
前記プログラムの実行直後において成立する不変条件を前記事後条件として前記事後条件記憶部に格納し、
前記プログラムの実行直前において成立する不変条件を前記論理式として前記論理式集合記憶部に格納する
解析処理部
をさらに備えたことを特徴とする請求項１又は２に記載の事前条件生成装置。
【請求項４】
前記プログラムを一部に含む第３のプログラムを記憶する親プログラム記憶部と、
前記第３のプログラムの事前条件および事後条件を記憶する親プログラム仕様記憶部と、
前記第３のプログラムの事前条件が成り立つときに前記第３のプログラムが実行された直後に前記第３のプログラムの事後条件が成立するという命題が成立するか否かを、前記命題の反例が存在するか否かを検査することにより判定するプログラム検査部と、を備え、
前記プログラム検査部は、前記第３のプログラムに含まれる前記プログラムは前記出力部により出力される事前条件、および前記事後条件記憶部内の事後条件を満たすことを仮定して検査を行う
ことを特徴とする請求項１ないし３のいずれか一項に記載の事前条件生成装置。
【請求項５】
命令型プログラミング言語によって記述されたプログラムを記憶するプログラム記憶部と、
１つ以上の論理式の論理積である、前記プログラムの事前条件を記憶する事前条件記憶部と、
前記事前条件が成立するときに前記プログラムが実行された直後に少なくともその要素の一つが満たされる必要のある、１つ以上の論理式の集合である必須条件を複数記憶する必須条件記憶部と、
複数の論理式を記憶する論理式集合記憶部と、
前記論理式集合記憶部から選択して組み合わせた１つ以上の前記論理式の集合である候補条件を前記必須条件と共通要素を持つように生成する候補条件生成部と、
前記事前条件が成り立つときに前記プログラムが実行されたならば前記候補条件の論理積が成立するという命題が成立するか否かを前記命題の反例が存在するか否かを検査することにより判定し、前記命題の反例が存在しないとき前記命題が成立し、前記命題の反例が存在するとき前記命題が成立しないことを決定する判定する第１の判定部と、
前記命題が成立すると決定された前記候補条件の論理積を、前記プログラムの事後条件として出力する出力部と、
を備えた事後条件生成装置。
【請求項６】
前記論理式集合記憶部内の論理式を１つ以上組み合わせることにより部分集合Ｚを生成する部分集合生成部と、
前記事前条件が成り立つときに前記プログラムが実行された直後に、前記論理式集合記憶部内の全論理式の集合Ｓから前記部分集合Ｚを除外した部分集合Ｓ−Ｚの論理積が成り立つという命題が成立するか否かを前記命題の反例が存在するか否かを検査することにより判定する第２の判定部と、をさらに備え、
前記必須条件記憶部は、前記第２の判定部により前記命題が成立しないと判定された前記第２の部分集合Ｚを前記必須条件として記憶する
ことを特徴とする請求項５に記載の事後条件生成装置。
【請求項７】
前記プログラムを一部に含む第２のプログラムを実行し、
前記第２のプログラムに含まれる変数の値の推移であるログを記録し、
前記ログに基づいて前記プログラムの実行直前および直後において成立する不変条件を生成し、
前記プログラムの実行直後において成立する不変条件を前記論理式として前記論理式集合記憶部に格納し、
前記プログラムの実行直前において成立する不変条件を前記事前条件として前記事前条件記憶部に格納する
解析処理部
をさらに備えたことを特徴とする請求項５又は６に記載の事後条件生成装置。
【請求項８】
前記プログラムを一部に含む第３のプログラムを記憶する親プログラム記憶部と、
前記第３のプログラムの事前条件および事後条件を記憶する親プログラム仕様記憶部と、
前記第３のプログラムの事前条件が成り立つときに前記第３のプログラムが実行された直後に前記第３のプログラムの事後条件が成立するという命題が成立するか否かを、前記命題の反例が存在するか否かを検査することにより判定するプログラム検査部と、を備え、
前記プログラム検査部は、前記第３のプログラムに含まれる前記プログラムは前記事前条件記憶部内の事前条件、および前記出力部により出力される事後条件、を満たすことを仮定して検査を行う
ことを特徴とする請求項５ないし７のいずれか一項に記載の事後条件生成装置。
【請求項９】
命令型プログラミング言語によって記述されたプログラムを記憶するプログラム記憶部と、
１つ以上の論理式の論理積である、前記プログラムの事後条件を記憶する事後条件記憶部と、
前記事後条件が成立するために前記プログラムの実行直前において少なくともその要素の一つが満たされる必要のある、１つ以上の論理式の集合である必須条件を複数記憶する必須条件記憶部と、
複数の論理式を記憶する論理式集合記憶部と、
にアクセスするステップと、
前記論理式集合記憶部から選択した１つ以上の前記論理式の集合である候補条件を前記必須条件と共通要素を持つように生成する候補条件生成ステップと、
前記候補条件の論理積が成り立つときに前記プログラムが実行された直後に前記事後条件が成立するという命題が成立するか否かを、前記命題の反例が存在するか否かを検査することにより判定し、前記命題の反例が存在しないとき前記命題が成立し、前記命題の反例が存在するとき前記命題が成立しないことを決定する第１の判定ステップと、
前記命題が成立すると決定された前記候補条件の論理積を、前記プログラムの事前条件として出力する出力ステップと、
を備えた事前条件生成方法。
【請求項１０】
命令型プログラミング言語によって記述されたプログラムを記憶するプログラム記憶部と、
１つ以上の論理式の論理積である、前記プログラムの事前条件を記憶する事前条件記憶部と、
前記事前条件が成立するときに前記プログラムが実行された直後に少なくともその要素の一つが満たされる必要のある、１つ以上の論理式の集合である必須条件を複数記憶する必須条件記憶部と、
複数の論理式を記憶する論理式集合記憶部と、
にアクセスするステップと、
前記論理式集合記憶部から選択して組み合わせた１つ以上の前記論理式の集合である候補条件を前記必須条件と共通要素を持つように生成する候補条件生成ステップと、
前記事前条件が成り立つときに前記プログラムが実行されたならば前記候補条件が成立するという命題が成立するか否かを前記命題の反例が存在するか否かを検査することにより判定し、前記命題の反例が存在しないとき前記命題が成立し、前記命題の反例が存在するとき前記命題が成立しないことを決定する判定する第１の判定ステップと、
前記命題が成立すると決定された前記候補条件の論理積を、前記プログラムの事後条件として出力する出力ステップと、
を備えた事後条件生成方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、命令型プログラミング言語を用いて記述された計算機プログラムの事前条件および事後条件を生成する、事前条件生成装置および事後条件生成装置、ならびにこれらの方法に関する。
【背景技術】
【０００２】
命令型プログラミング言語におけるプログラムの仕様や性質を表す基本的な方法として、プログラムの事前条件・事後条件の組を用いる方法が知られている。また、その背景となる理論として、プログラムの事前条件・事後条件を、公理と推論規則によって導出することでプログラムの正当性を示す方法論である公理的意味論が知られている。公理的意味論の具体例としてホーア論理が知られている。
【０００３】
特開2005-182806号公報は、ある与えられた仕様を満たすプログラムを生成する方法について述べており、仕様の記述方法の一つとして公理的意味論を用いたものが想定されている。
【先行技術文献】
【特許文献】
【０００４】
【特許文献１】特開2005-182806号公報
【発明の概要】
【発明が解決しようとする課題】
【０００５】
上述した公理的意味論を用いてプログラムの検証などを行う際には、プログラム中の各部分における事前条件・事後条件が全て与えられているとは限らない。そのような場合にはプログラム中の当該各部分の前後の情報を利用して最弱事前条件や最強事後条件を計算する（最弱事前条件や最強事後条件を伝播によって求める）ことが望ましい。例えば、代入文「x := x + 1;」の事後条件が「x > 10」であれば、その最弱事前条件は「x > 9」となる。しかし、最弱事前条件や最強事後条件を自動的に計算することが常に容易とは限らない。
【０００６】
その理由の一つとして、プログラム中にループが存在した場合、ループ内部の実行前後で常に成り立つ条件であるループ不変条件(loop invariant)を自動的に導出することが必要であるが、(一般に用いられている命令型プログラミング言語では)これは決定可能ではないことが知られている(A. Blass and Y. Gurevich.  Inadequacy of Computable Loop Invariants. ACM Transactions on Computational Logic. 2(1): 1-11, January 2001.)。
【０００７】
ループ不変条件を自動的に推定するための研究も行われている（例えば、N. Suzuki, and K. Ishihata.  Implementation of an Array Bound Checker. 4th ACM Symposium on Principles of Programming Languages. Los Angeles, CA (January 1977).）が、計算量の問題や、適用範囲が限られるといった問題から、広く使われるには至っていない。
【０００８】
本発明は、プログラムの事後条件が事前に与えられた場合に当該プログラムの事前条件を効率よく近似的に生成することを可能とした事前条件生成装置およびその方法、ならびに、プログラムの事前条件が事前に与えられた場合に当該プログラムの事後条件を効率よく近似的に生成することを可能とした事後条件生成装置およびその方法を提供する。
【課題を解決するための手段】
【０００９】
本発明の一態様としての事前条件生成装置は、
命令型プログラミング言語によって記述されたプログラムを記憶するプログラム記憶部と、
１つ以上の論理式の論理積である、前記プログラムの事後条件を記憶する事後条件記憶部と、
前記事後条件が成立するために前記プログラムの実行直前において少なくともその要素の一つが満たされる必要のある、１つ以上の論理式の集合である必須条件を複数記憶する必須条件記憶部と、
複数の論理式を記憶する論理式集合記憶部と、
前記論理式集合記憶部から選択した１つ以上の前記論理式の集合である候補条件を前記必須条件と共通要素を持つように生成する候補条件生成部と、
前記候補条件の論理積が成り立つときに前記プログラムが実行された直後に前記事後条件が成立するという命題が成立するか否かを、前記命題の反例が存在するか否かを検査することにより判定し、前記命題の反例が存在しないとき前記命題が成立し、前記命題の反例が存在するとき前記命題が成立しないことを決定する第１の判定部と、
前記命題が成立すると決定された前記候補条件の論理積を、前記プログラムの事前条件として出力する出力部と、
を備える。
【００１０】
本発明の一態様としての事後条件生成装置は、
命令型プログラミング言語によって記述されたプログラムを記憶するプログラム記憶部と、
１つ以上の論理式の論理積である、前記プログラムの事前条件を記憶する事前条件記憶部と、
前記事前条件が成立するときに前記プログラムが実行された直後に少なくともその要素の一つが満たされる必要のある、１つ以上の論理式の集合である必須条件を記憶する必須条件記憶部と、
複数の論理式を記憶する論理式集合記憶部と、
前記論理式集合記憶部から選択して組み合わせた１つ以上の前記論理式の集合である候補条件を前記必須条件と共通要素を持つように生成する候補条件生成部と、
前記事前条件が成り立つときに前記プログラムが実行されたならば前記候補条件の論理積が成立するという命題が成立するか否かを前記命題の反例が存在するか否かを検査することにより判定し、前記命題の反例が存在しないとき前記命題が成立し、前記命題の反例が存在するとき前記命題が成立しないことを決定する判定する第１の判定部と、
前記命題が成立すると決定された前記候補条件の論理積を、前記プログラムの事後条件として出力する出力部と、
を備える。
【００１１】
本発明の一態様としての事前条件生成方法は、
命令型プログラミング言語によって記述されたプログラムを記憶するプログラム記憶部と、
１つ以上の論理式の論理積である、前記プログラムの事後条件を記憶する事後条件記憶部と、
前記事後条件が成立するために前記プログラムの実行直前において少なくともその要素の一つが満たされる必要のある、１つ以上の論理式の集合である必須条件を複数記憶する必須条件記憶部と、
複数の論理式を記憶する論理式集合記憶部と、
にアクセスするステップと、
前記論理式集合記憶部から選択した１つ以上の前記論理式の集合である候補条件を前記必須条件と共通要素を持つように生成する候補条件生成ステップと、
前記候補条件の論理積が成り立つときに前記プログラムが実行された直後に前記事後条件が成立するという命題が成立するか否かを、前記命題の反例が存在するか否かを検査することにより判定し、前記命題の反例が存在しないとき前記命題が成立し、前記命題の反例が存在するとき前記命題が成立しないことを決定する第１の判定ステップと、
前記命題が成立すると決定された前記候補条件の論理積を、前記プログラムの事前条件として出力する出力ステップと、
を備える。
【００１２】
本発明の一態様としての事後条件生成方法は、
命令型プログラミング言語によって記述されたプログラムを記憶するプログラム記憶部と、
１つ以上の論理式の論理積である、前記プログラムの事前条件を記憶する事前条件記憶部と、
前記事前条件が成立するときに前記プログラムが実行された直後に少なくともその要素の一つが満たされる必要のある、１つ以上の論理式の集合である必須条件を複数記憶する必須条件記憶部と、
複数の論理式を記憶する論理式集合記憶部と、
にアクセスするステップと、
前記論理式集合記憶部から選択して組み合わせた１つ以上の前記論理式の集合である候補条件を前記必須条件と共通要素を持つように生成する候補条件生成ステップと、
前記事前条件が成り立つときに前記プログラムが実行されたならば前記候補条件の論理積が成立するという命題が成立するか否かを前記命題の反例が存在するか否かを検査することにより判定し、前記命題の反例が存在しないとき前記命題が成立し、前記命題の反例が存在するとき前記命題が成立しないことを決定する判定する第１の判定ステップと、
前記命題が成立すると決定された前記候補条件の論理積を、前記プログラムの事後条件として出力する出力ステップと、
を備える。
【発明の効果】
【００１３】
本発明により、プログラムの事後条件が事前に与えられた場合に、当該プログラムの事前条件を効率よく近似的に生成することが可能となる。また本発明により、プログラムの事前条件が事前に与えられた場合に、当該プログラムの事後条件を効率よく近似的に生成することが可能となる。生成した事前条件および事後条件は、プログラムの検証などに用いることが出来る。
【図面の簡単な説明】
【００１４】
【図１】本発明の一実施の形態に従った事前条件生成装置の基本構成を示す図。
【図２】図１の装置による前処理の流れを示すフローチャート。
【図３】図１の装置による本処理の流れを示すフローチャート。
【図４】前処理の流れを命令型言語の擬似コードで記述した例を示す図。
【図５】本処理の流れを命令型言語の擬似コードで記述した例を示す図。
【図６】ハッセ図の例を示す図。
【図７】結果利用部の詳細構成を示す図。
【発明を実施するための形態】
【００１５】
以下、図面を適宜参照しながら、本発明の実施の形態について詳細に説明する。
【００１６】
まず、用語と記法の定義について説明する。
【００１７】
（１）本明細書では、論理式の有限集合Sに対して、その要素全ての論理積を ∧S と記述する。S={A,B,C} であれば ∧S は A∧B∧C のことである。S=φ のときには ∧S は恒真な論理式 true のことである。また、∧{X1, X2, X3, …, Xn}のことを単に∧Xiと書く。
【００１８】
（２）事前条件, 事後条件
論理式P が成り立っている状態でプログラムCを実行し、実行が終了した場合には終了状態で常に論理式Qが成り立っているとする(プログラムCが終了することは要求されていない)。このとき、論理式PをプログラムCの事前条件、論理式QをプログラムCの事後条件と呼ぶ。また、この関係（命題）がなりたっていることを {P} C {Q} と記述する。
【００１９】
（３）必須条件
論理式Qが与えられているとする。論理式集合 S の部分集合Xに関して、{∧ (S-X)} C {Q} が成り立たないときに、部分集合Xは必須条件と呼ぶ。
【００２０】
これはXに含まれないSの要素をいくら事前条件に追加してもQを成り立たせることがないという意味でXの要素が必須であるためである。ただし、Ｘの要素はQを成り立たせるための十分条件とは限らないため、Xの要素を全て事前条件に追加してもQが成り立つとは限らない。
【００２１】
（４）本明細書では有限集合しか扱わないため、その部分集合は各要素が含まれているか否かを表すビットの列によって効率的に表現できる。例えば、S={a,b,c}という集合が与えられたときに、{a,b,c}, {a,c}, {a}, φ という部分集合はそれぞれ 111, 101, 100, 000 というビット列によって表現できる。本実施形態の装置では、部分集合は、内部的にビット列で表現され処理されるものとする。
【００２２】
図１は、本発明の一実施の形態に従った事前条件生成装置の基本構成を示す。
【００２３】
この装置は、候補論理式集合記憶部（論理式集合記憶部）１１と、小規模部分集合Z生成部（部分集合生成部）１２と、S-Z事後条件成立判定部（第２の判定部）１３と、必須条件集合記憶部（必須条件記憶部）１４と、プログラム記憶部１５と、部分集合列挙部１６と、矛盾性検査部１７と、事後条件成立判定部（第１の判定部）１８と、枝狩り用集合記憶部（枝狩り用条件記憶部）１９と、事後条件記憶部２０と、出力部２１と、出力を実際の検証に利用する結果利用部２２とを備える。部分集合列挙部１６と矛盾性検査部１７との組はたとえば本発明の候補条件生成部１０をなす。
【００２４】
本装置による処理は大きく前処理と本処理と出力を利用した処理に分けられる。以下、前処理および本処理の概要を説明し、その後、具体例を用いてさらに詳しく説明する。最後に出力を利用した検証処理について説明を行う。
【００２５】
図２は前処理の流れを示すフローチャート、図３は前処理の後に行われる本処理の流れを示すフローチャートである。
【００２６】
ただし、前処理の前に、プログラム記憶部１５に対象となるプログラムを、事後条件記憶部２０に事後条件Qを、候補論理式集合記憶部１１に有限個の論理式の集合S をあらかじめ記憶させておく。候補論理式集合記憶部１１内の論理式は、最終的に生成される事前条件を形成する部品の候補となるものである。
【００２７】
図２に示すように、まず、必須条件集合記憶部１４および枝狩り用集合記憶部１９を初期化する（ステップS11）。すなわち、必須条件集合記憶部１４内の必須条件集合 ζを空集合 φ にし、枝刈り用集合記憶部１９内の枝刈り用集合 Ψを空集合 φにする。初期化は、図１の装置に初期化手段を追加的に設けてこれにより行ってもよいし、図１の任意の要素に初期化手段の機能を内部的に備えさせ、これにより行ってもよい。
【００２８】
次に、小規模部分集合Z生成部１２が、候補論理式集合記憶部１１に記録された集合Sから、その小さな部分集合 Z1, Z2, … ⊆ S を、適当な個数だけ生成する。たとえば所定サイズ以下の部分集合をすべて生成する（ステップS12）。
【００２９】
S-Z事後条件成立判定部１３は生成された各ZiからZiを順次選択し（ステップS13）、論理式の集合Ziが必須条件であるか否かを検査する（ステップS14）。より詳細にはSからZiを除いた集合 S-Zi に対して、{∧(S-Zi)} C {Q} が反例を持つかを検査し、反例が見つかったときはその集合Ziは必須条件、見つからないときはその集合Ziは必須条件でないと判断する(処理の詳細は後述する図３のステップS25の説明を参照)。
【００３０】
S-Z事後条件成立判定部１３は、反例が見つかった場合には（YES）、Zi を 必須条件集合記憶部１４内の集合 ζ に加える(ζ を ζ∪{ Zi} で置き換える)（ステップS15）。まだ選択していないZiが存在するかどうかを検査し（ステップS16）、まだ存在するときは（YES）、次のZiを選択するステップS13に戻り、すべてのZiを選択済みのときは（NO）、本処理を終了する。
【００３１】
一方、ステップS14において、反例が発見されなかった場合には（NO）、何も行わず、次のZiを選択するステップS13に戻る。
【００３２】
図４に、全体集合Sからサイズが3以下の部分集合を全てZ1, Z2, … として生成し、反例を持つものを必須条件集合記憶部１４内の集合ζに追加する処理を命令型言語の擬似コードで記述した例を示す。この例では、最初、集合 ζが空集合φである状態に初期化され、この後、f(1, φ),f(2, φ),f(3, φ)が順次実行される。f(n,Z)の「n」は部分集合のサイズを示している。
【００３３】
以上により前処理が完了し必須条件集合記憶部１４に必須条件が記憶される。この後、本処理を行う。以下、図３のフローチャートに基づいて本処理について説明する。
【００３４】
基本的な流れは、ステップS21で部分集合列挙部１６がSの部分集合X1,X2,…⊆Sを順次生成し、生成されたものから順次検査を行い、矛盾性検査部１７および事後条件成立判定部１８により許可された部分集合の論理積を事前条件として出力するという流れになっている。この流れを命令型言語の擬似コードとして示した一例を図５に示す。
【００３５】
ステップS21では、 部分集合列挙部１６が、候補論理式集合記憶部１１内の論理式（部品）を１つ以上組み合わせることにより、部分集合を１つ生成する。後述のステップS22のYES、またはステップS28を介して本ステップS21へ戻るごとに部分集合を１つ生成する。このようにして部分集合列挙部１６は部分集合X1,X2,…⊆Sを順次生成する。なお、本ステップS21において生成すべき部分集合がもはや存在しないと判断したときは本フローの処理を終了する。生成した部分集合は本発明の候補条件に相当し、したがって部分集合列挙部１６は、候補論理式集合記憶部１１から選択した１つ以上の論理式の集合である候補条件を生成しているといえる。ここで、部分集合の生成順序は X⊆Yならば、XがYよりも先に生成されるような順序で生成を行うという順序制約を満たすものとする。以下、この順序制約の詳細について説明する。
【００３６】
図６はS={a,b,c} の場合に、包含関係に基づいて候補集合をハッセ図として示したものである。ハッセ図においては、節点Yを上部、節点Xを下部とする辺の存在は、X⊆Y であることを表しており、反射律と推移律で導出可能なものを除いた包含関係が図示されている。
【００３７】
前述の順序制約を満たす列挙方法の一つは、このハッセ図の下側から幅優先探索によって列挙することである。その場合には、φ, {a}, {b}, {c}, {a,b}, {a,c}, {b,c}, {a,b,c} という順番で列挙が行われる。
【００３８】
また、前述の順序制約を満たす限りにおいては別の順序であっても構わない。一例として、φ, {a}, {b}, {a,b}, {c}, {a,c}, {b,c}, {a,b,c} という順序がそれにあたる。
【００３９】
ステップS22では、部分集合列挙部１６が、ステップS21で生成した部分集合（組み合わせ）が、枝狩り用集合記憶部１９内の枝刈り用集合を含む否かを検査する。より詳細には、当該部分集合が、枝狩り用集合を含むか否かを検査する。
【００４０】
すなわち、ステップS21で生成された部分集合 X⊆S に対して、P⊆X であるPが存在するかを検査する。ここでPは枝刈り用集合であり、枝狩り用集合記憶部１９内のすべての枝狩り用集合をΨと表すと、P∈Ψ である。そのようなPが存在した場合には（YES）、当該部分集合Xを破棄し、ステップS21に戻り次の候補（部分集合）を、前述した順序制約を満たすように生成する。そのようなPが存在しない場合には（NO）、次のステップS23へと進む。
【００４１】
ここで、枝刈り用集合Pは、Pに含まれる論理式間に矛盾がある集合、すなわちPに含まれる論理式の論理積が矛盾する集合（後述するステップS24で矛盾すると判断された集合）もしくは既に出力済みの集合（後述するステップS26で出力された集合）であり、本ステップS22ではこのような枝狩り用集合Pを含む部分集合を排除している。 論理式間に矛盾を含む集合を含む部分集合を排除するのは、そのような部分集合自体も矛盾し、そのような部分集合を満たすプログラムの実行状態は存在しないため、そのような部分集合を事前条件として考えることには意味がないからである。一方、既に出力済みの集合を含むような部分集合を排除するのは、そのような部分集合は、条件を満たす極小な集合ではなく、出力する意味に乏しいためである。
【００４２】
ステップS23では、ステップS22において枝狩り用集合Pを含まないと判断された部分集合Xが、必須条件集合の各要素（必須条件）Zをすべて含むか否かを、部分集合列挙部１６において検査する（部分集合Xが、Zに含まれる論理式を含むか否かをZ毎に検査する）。すなわち、各部分集合Z∈ζについて、部分集合X が部分集合Zを含むか否かを検査する。X に含まれないようなZ∈ζが存在する場合には（NO）、そのようなXは破棄し、ステップS21に戻り、次の候補（部分集合）の生成に移る。全てのZ∈ζについてXがZとの間に共通要素を持つ場合には（YES）、次のステップS24へと進む。このように、必須条件集合の各要素のうち１つでも含まない候補（部品集合X）については本ステップで排除することにより、以降のステップでの計算量を低減できる。すなわちこのような候補は、いずれにしても後のステップS25で廃棄される可能性が高いが、本ステップでは計算量が少なくて済むため、本ステップで前もって廃棄しておく。ここではすべてのZとXが共通要素を持つ含むことを要求したが、少なくとも１つのZがXとの間に共通要素を持つことを条件としてステップS24へ進むように処理を変更するようにしてもよい。
【００４３】
ステップS24では、矛盾性検査部１７が、部分集合（組み合わせ）Xに含まれる論理式間に矛盾が存在するか否かを検査する（すなわち候補条件である部分集合Xの論理積が矛盾するか否かを検査する）。矛盾が発見された場合は、当該部分集合を枝刈り用集合として登録する（当該候補条件を枝狩り用条件として登録する）ステップS28へと移る。矛盾が発見されなかった場合には、次のステップS25へと進む。矛盾を発見する方法としては、∧Xを満たす状態を探索することによって行う方法があり、SATソルバーなどを用いることが出来る。このように矛盾する事前条件を本ステップで除外することで、矛盾を含む事前条件を出力しないようにする。そのため、矛盾を含む事前条件が出力されることが許容される場合には、矛盾を常に検出可能とは限らない検査方法を用いても問題は無い。
【００４４】
ステップS25では、事後条件成立判定部１８が、部分集合Xの論理積が成り立つときにプログラム記憶部１５内のプログラムを実行した直後に、事後条件記憶部２０内の事後条件の論理積が成立するという命題が成立するか否かを検査する。より詳細に、{∧X} C {Q} の命題が成立するか否かの検査を、{∧X} C {Q} の反例を探索することによって行う。{∧X} C {Q} の反例の探索は、Cの実行例で、実行前の状態で∧X が成り立ち、実行後の状態で Q が成り立たないものを見つけることで行う。そのような実行例が存在すれば {∧X} C {Q} は成り立たない。
【００４５】
そのような探索を行うための方法として、米国マサチューセッツ工科大学の Daniel Jacksonらのグループによる方法(Greg Dennis, Felix Sheng-Ho Chang, and Daniel Jackson. Modular verification of code with sat. In ISSTA ’06: Proceedings of the 2006 international symposium on Software testing and analysis, pp. 109.120, New York, NY, USA, 2006. ACM.)を用いることが出来る。また、この方法を具体化したツールとして、同グループによって開発されている Forge (http://sdg.csail.mit.edu/forge/)  を用いることが出来る。また、別の方法としてモデル検査で用いられている手法を用いることが出来るが、これらの方法の詳細は本発明の主眼ではないため、ここではこれ以上述べない。
【００４６】
{∧X} C {Q} に反例が存在することがわかった場合（NO）、事後条件成立判定部１８は部分集合Xを破棄し、ステップS21に戻る。反例が見つからなかった場合、すなわち部分集合X が {∧X} C {Q} を成り立たせる場合には（YES）、次のステップS26へと進む。
【００４７】
ステップS26では、出力部２１が、ステップS25で事後条件を成立させると判断された部分集合Xを出力する（すなわち当該部分集合Xの論理積である候補条件を事前条件として出力する）。
【００４８】
ステップS27では、事後条件成立判定部１８が、さらに答え（出力）が必要か否かを判断する。判断の方法としては、たとえば所定数の部分集合（すなわち所定数の事前条件）が出力されたか否か、もしくは出力がユーザーである人間によって直接用いられる場合には、ユーザーに継続するか中断するかの判断を行わせることによって、行うことができる。
【００４９】
さらに答え（出力）が必要でない場合は（NO）、ここで本処理を終了する。答え（出力）がさらに必要な場合には、部分集合Xを枝刈り用集合に加えるステップS28へと移る。ここで、Xを枝刈り用集合として登録するのは、以降に生成される可能性のある(Xを部分集合として含むような)冗長な候補（部分集合）を事前に取り除くためである。
【００５０】
ステップS28では、ステップS24で矛盾すると判断された部分集合X、ステップS25で事後条件を成立させると判断された部分集合Xを、枝刈り用集合に追加する(ΨをΨ∪{X}で置き換える)。ステップS28の実行後は、ステップS21に戻り、次の候補Xの生成へと移る。
【００５１】
上記ステップS24における矛盾性検査によって候補（部分集合）Xが矛盾することが発見された場合に、Xのどの部分集合Yが矛盾しているのかを調べ、X自体の代わりにYを枝刈り集合として登録するようにしてもよい。このように、より小さな部分集合を登録することによって、より早期に枝刈りを行うことが可能になり、性能の向上が見込まれる。なお、反駁証明を行う定理証明器では、どの部分集合が矛盾するのかを抽出する機能を持つものが存在しているため、そのような定理証明器を矛盾検査に利用することが出来る。
【００５２】
また図３の処理のフローでは、部分集合列挙部１６で部分集合を生成した後で当該部分集合が必須条件を含むか否かを判断し、必須条件を含まないときは当該部分集合を廃棄したが、最初から必須条件を含むように部分集合を生成し、必須条件を含むか否かの判断を行わないようにしてもよい。いずれの場合も、必須条件を含むような部分集合を矛盾性検査部１７に渡すことに代わりはないため、どちらの方法を採用しても問題はない。
【００５３】
以下では、命令型言語で記述された以下のようなプログラムに対して、本実施の形態の処理を行う例について述べる。
【表１】
2010218148.tif 000003
【００５４】
このプログラムは変数xの絶対値を計算し、変数yへと格納するプログラムである。このプログラムを以下、Cとして表現する。このプログラムがプログラム記憶部１５に記憶されている。
【００５５】
さらに、事後条件として y≦5 が事後条件記憶装２０に記憶され、事前条件の部品候補として以下の4つの論理式が候補論理式集合記憶部１１に記憶されているとする。
【００５６】
a：x≦5
b：x≦10
c：10≦x
d：-5≦x
まず以下のように前処理を行うことにより必須条件を登録する。
【００５７】
必須条件集合記憶装置１４および枝狩り用集合記憶装置１９を初期化し（図１のステップS11）、小規模部分集合Z生成部１２において部分集合Zを生成する（ステップS12）。ここでは説明の簡単化のために、Zの要素数が1以下の場合を考えることとする。すなわち、小規模部分集合Z生成部１２は、φ,{a},{b},{c},{d}の５個のZを生成する（ステップS12）。
【００５８】
この後、S-Z事後条件成立判定部１３において、まずZ=φを選択し（ステップS13）、∧(S-Z) = ∧{a,b,c,d} = a∧b∧c∧d となり、{a∧b∧c∧d} C {y≦5} に反例が存在するか検査する。ここで a の x≦5 と c の 10≦x は矛盾するため、事前条件 a∧b∧c∧d を満たす状態は存在せず、したがって Cの実行前に a∧b∧c∧d を満たしてかつ C の実行後に y≦5 が成立しないような場合というのは存在しない。そのため、反例は発見されない。したがって、Z=φは、必須条件ではなく（ステップS14のNO）、必須条件集合記憶部１４に登録されない。
【００５９】
次に Z={a} を選択し（ステップS13）、{b∧c∧d} C {y≦5} に反例が存在するか検査を行う。x=10のときには b∧c∧d が成り立ち、かつ C の実行後には y=10 となって y≦5 を満たさない。したがって、実行前にx=10 で実行後にy=10 である場合が反例として発見される。反例が発見されたため、{a}は必須条件であり、（ステップS14のYES）、{a} を必須条件として登録する（ステップS15）。すなわちZ={a}は必須条件集合記憶部１４に登録される。
【００６０】
次に Z={b} を選択し（ステップS13）、{a∧c∧d} C {y≦5} に反例が存在するか検査を行う。この場合、Z=φの場合と同様に、a∧c∧d を満たす状態は存在しないため反例は発見されない。したがってZ={b}は、必須条件ではなく（ステップS14のNO）、必須条件集合記憶部１４に登録されない。
【００６１】
次に Z={c} を選択し（ステップS13）、{a∧b∧d} C {y≦5} に反例が存在するか検査を行う。この場合、a∧b∧d を満たす状態というのは -5≦x≦5 である状態であり、この場合には C の実行後には y≦5 は必ず成り立つため反例は発見されない。したがってZ={c}は必須条件ではなく（ステップS14のNO）、必須条件集合記憶部１４に記憶されない。
【００６２】
次に Z={d} を選択し（ステップS13）、{a∧b∧c} C {y≦5} に反例が存在するか検査を行う。この場合、Z=φの場合と同様に、a∧b∧d を満たす状態は存在しないため反例は発見されない。したがってZ={d}は、必須条件ではなく（ステップS14のNO）、必須条件集合記憶部１４に登録されない。
【００６３】
以上によりすべてのZが選択されたため（ステップS16のNO）、前処理を終了する。前処理の結果、必須条件集合ζは{{a}}となり、これが必須条件集合記憶部１４に記憶されることとなる。
【００６４】
次に、本処理を行う。
【００６５】
部分集合列挙部１６における部分集合の列挙順序（生成順序）を決める必要があるが、ここでは φ, {a}, {b}, {a,b}, {c}, {a,c}, {b,c}, {a,b,c}, {d}, {a,d}, {b,d}, {a,b,d}, {c,d}, {a,c,d}, {b,c,d}, {a,b,c,d} の順番で候補（部分集合）が生成されるものとする（図２のステップS21）。以下、各候補に対して順番に処理を行った結果を述べる。
【００６６】
まず、φ は、必須条件{a}との共通要素を持たないため（図３のステップS23のNO）、破棄される。
【００６７】
{a} は全ての必須条件との間に共通要素を持っており（ステップS23のYES）、矛盾もしないが（ステップS24の無矛盾）、x=-6が {a} C {y≦5} の反例となるため、事後条件成立の検査に失敗し（ステップS25のNO）、破棄される。
【００６８】
{b} は必須条件 {a} との共通要素を持たないため（ステップS23のNO）、破棄される。
【００６９】
{a,b} は全ての必須条件との間に共通要素を持っているが（ステップS23のYES）、x=-6 が {a∧b} C {y≦5} の反例となるため、事後条件成立の検査に失敗し（ステップS25のNO）、破棄される。
【００７０】
{c} は必須条件 {a} との共通要素を持たないため（ステップS23のNO）、破棄される。
【００７１】
{a,c} は全ての必須条件との間に共通要素を持っているが（ステップS23のYES）、a の x≦5 と c の 10≦x とが矛盾するため（ステップS24の矛盾）、枝刈り用集合として {a,c} を登録する（ステップS28）。
【００７２】
{b,c} は必須条件 {a} との間の共通要素を持たないため（ステップS23のNO）、破棄される。
【００７３】
{a,b,c} は、枝刈り用集合 {a,c} を含んでいるため（ステップS22のYES）、破棄される。
【００７４】
{d} は必須条件 {a} との間に共通要素を持たないため（ステップS23のNO）、破棄される。
【００７５】
{a,d} は、枝刈り用集合を含んでおらず（ステップS22のNO）、全ての必須条件との間に共通要素を持っており（ステップS23のYES）、矛盾もせず（ステップS24の無矛盾）、{a∧d} C {y≦5}に反例も発見されないため（ステップS25のYES）、{a,d} すなわち {ｘ≦5, -5≦x }を事前条件として出力する（ステップS26）。さらに答えが必要か判断し（ステップS27）、不要であると判断された場合には（NO）ここで処理を終了する。さらに答えが必要と判断される場合には（YES）、{a,d} を枝刈り用集合として登録し（ステップS28）、次の候補を生成する（ステップS21）。
【００７６】
{b,d} は必須条件 {a} との間に共通要素を持たないため（ステップS23のNO）、破棄される。
【００７７】
{a,b,d} は枝刈り用集合 {a,d} を含むため（ステップS22のYES）、破棄される。
【００７８】
{c,d} は必須条件 {a} との間に共通要素を持たないため（ステップS23のNO）、破棄される。
【００７９】
{a,c,d} は枝刈り用集合の{a,c}または {a,d}を含むため（ステップS22のYES）、破棄される。
【００８０】
{b,c,d} は必須条件 {a} との間に共通要素を持たないため（ステップS23のNO）、破棄される。
【００８１】
{a,b,c,d} は枝刈り用集合の {a,c}または{a,d} を含むため（ステップS22のYES）、破棄される。
【００８２】
以上で本処理が終了する。
【００８３】
これまでの説明では、事後条件記憶部２０に事後条件を、候補論理式集合記憶部１１に事前条件の部品（論理式）をあらかじめ記憶させておいたが、これら事前条件の部品（論理式）および事後条件を自動生成する機能（解析処理部）を図１の装置に追加してもよい。この機能の実現には、たとえばマサチューセッツ工科大学のM. Ernstの研究グループが開発したDaikon(“The Daikon system for dynamic detection of likely invariants” by Michael D. Ernst, Jeff H. Perkins, Philip J. Guo, Stephen McCamant, Carlos Pacheco, Matthew S. Tschantz, and Chen Xiao. Science of Computer Programming, vol. 69, no. 1--3, Dec. 2007, pp. 35-45.)を用いることができる。
【００８４】
Daikonは、プログラムを実行させプログラム中での変数の遷移をログとして記録する機能を持ち、そのログに対して機械学習の技術を用いて解析することで、サブルーチンの入り口および出口などでの条件制約になっていると思われる条件（不変条件）を抽出することが出来る。
【００８５】
そこで、Daikonを用いてあるサブルーチン（あるプログラム）を含む第２のプログラムを実行し、当該あるサブルーチン（あるプログラム）の実行前と実行後の条件制約と思われる候補（不変条件）を取得し、Daikonから得たサブルーチン実行後の条件制約と思われる不変条件を、事後条件として事後条件記憶部２０に記憶し、Daikonから得たサブルーチン実行前の条件を、事前条件の部品（論理式）として候補論理式集合記憶部１１に記憶させる。この後は、既に述べた通りの前処理および本処理を行えばよい。
【００８６】
なお、図１の装置において、小規模部分集合Z生成部１２と部分集合列挙部１６はそれぞれ別個の装置として示しているが、これらは機能的に共通する部分があるためその部分については共通のモジュールとして共用してもよい。
【００８７】
また同様にS-Z事後条件成立判定部１３と事後条件成立判定部１８はそれぞれ別個の装置として示しているが、これらは機能的に共通する部分があるためその部分については共通のモジュールとして共用してもよい。
【００８８】
次に、結果利用部２２で行う検証処理について説明する。得られた事前条件・事後条件はプログラムの様々な検証に用いることが出来るため、その例を説明する。
【００８９】
一例としては、事前条件・事後条件を求めたプログラムCをサブルーチンとして利用する別のプログラムDの検証に利用することが挙げられる。
【００９０】
プログラム検証技術の中にはプログラムCが与えられた仕様(事前条件・事後条件)を満たすことを仮定することで、プログラムCの実装には全く立ち入らずにプログラムDの検証を行うことが出来るものが知られている(本明細書で先に述べたForgeもその一つである)。このような検証技術はプログラムの全体を同時に検査するのではなく、個々には小さな部品を単位として検証を行うため、大規模なプログラムに対しても適用しやすいという利点が存在している。
【００９１】
そこで、そのような検査技術を用いてプログラムDの検査を行う際に、本技術で求めた事前条件・事後条件をプログラムCの仕様として用いることで、プログラムCの完全な仕様(事前条件・事後条件)が存在しない場合についても、プログラムDの検証をプログラムCの実装に立ち入らず行うことが出来る。
【００９２】
この例での結果利用部２２のより詳細な構成を図7に示す。ここで親プログラム記憶部２４にプログラムDが記憶されており、親プログラム仕様記述部２５にプログラムDの仕様(事前条件・事後条件)が記述されている。プログラム検査部２３は親プログラム記憶部２４に記憶されたプログラムDが親プログラム仕様記述部２３に記憶された仕様を満たすかどうかの検査をステップＳ２４と同様の方法を用いて行う。ただし、その際にプログラムＤ内部で用いられているプログラムＣの部分については、プログラムＣの実装を参照することなく、出力部２１から与えられた条件を満たすものとして検査を行う。すなわち、プログラム検査部２３は、プログラムD（第３のプログラム）の事前条件が成り立つときにプログラムDが実行された直後にプログラムDの事後条件が成立するという命題が成立するか否かを、命題の反例が存在するか否かを検査することにより判定し、この際、プログラム検査部２３は、プログラムDに含まれるプログラムC（サブルーチン）は出力部２１により出力される事前条件、および事後条件記憶部２０内の事後条件を満たすことを仮定して検査を行う。これにより検査を短時間で効率的に行うことができる。
【００９３】
結果利用部２２で行う検証の別の例としては、得られた事前条件・事後条件とプログラムの元々の(自然言語で記述された)仕様との間に乖離がないかどうかを、人間のユーザーが確認・判断することが挙げられる。そして、乖離があると判断された場合には、仕様とプログラムの少なくとも一方には問題があるため、仕様とプログラムの一方ないしは両方を修正することになる。
【００９４】
一般に、プログラムが手順を記述したものであるのに対して、仕様は成り立つべき性質を記述したものであり、両者の書かれ方は全く異なっているためプログラムと仕様との間に乖離があるかは判断しにくい。しかし、この方法ではプログラムから事前条件・事後条件というより宣言的な条件記述を生成し、これを仕様と比較することで、乖離が存在するかをより容易に判断できる。
【００９５】
以上のように、本実施の形態により、プログラムの事後条件があらかじめ与えられた場合に、あらかじめ与えられた論理式の組み合わせることにより、当該プログラムの事前条件を効率よく近似的に求めることが可能となる。すなわち、ループ等の存在により最弱事前条件を自動的に計算することは一般的に出来ないが、本実施の形態では、事前条件の部品候補となる論理式の集合と、事後条件とがあらかじめ与えられたとき、無矛盾かつ事後条件を成立させるような論理式の組み合わせを探索することで、近似された事前条件を効率的に求めることができる。
【００９６】
これまで述べた本実施の形態は、事前条件と、事後条件の部品候補（論理式）とが事前に与えられた場合に、論理式を組み合わせることにより、事前条件を満足する事後条件を近似的に効率的に求める事後条件生成装置に拡張することも可能である。この場合の処理は基本的にこれまでの処理の説明において、必要に応じて「事後条件」と「事前条件」とを入れ替えて読むことで実現可能である。このような近似で得られる事後条件は、最強ではない事後条件(最強事後条件によって含意される条件)となる。
【符号の説明】
【００９７】
１１：候補論理式集合記憶部（論理式集合記憶部）
１２：小規模部分集合Z生成部（部分集合生成部）
１３：S-Z事後条件成立判定部（第２の判定部）
１４：必須条件集合記憶部（必須条件記憶部）
１５：プログラム記憶部
１６：部分集合列挙部（候補条件生成部）
１７：矛盾性検査部（候補条件生成部）
１８：事後条件成立判定部（第１の判定部）
１９：枝狩り用集合記憶部
２０：事後条件記憶部
２１：出力部
【図１】
2010218148.tif 000004
【図２】
2010218148.tif 000005
【図３】
2010218148.tif 000006
【図４】
2010218148.tif 000007
【図５】
2010218148.tif 000008
【図６】
2010218148.tif 000009
【図７】
2010218148.tif 000010