特許

J-GLOBAL ID：201003078962061228

事前条件生成装置および事後条件生成装置、ならびにこれらの方法

発明者： 酒 井 政 裕 ,  今 井 健 男
出願人/特許権者： 株式会社東芝
代理人 (5件)： 吉武 賢次 ,  佐藤 泰和 ,  吉元 弘 ,  川崎 康 ,  鈴木 順生
公報種別：公開公報
出願番号（国際出願番号）：特願2009-063253
公開番号（公開出願番号）：特開2010-218148
出願日： 2009年03月16日
公開日（公表日）： 2010年09月30日
要約：

【課題】プログラムの事後条件が事前に与えられた場合に当該プログラムの事前条件を効率よく近似的に生成することを可能とした事前条件生成装置およびその方法を提供する。【解決手段】事前条件生成装置は、プログラムを記憶するプログラム記憶部15と、前記プログラムの事後条件を記憶する事後条件記憶部と、1つ以上の論理式の集合である必須条件を複数記憶する必須条件記憶部と、複数の論理式を記憶する論理式集合記憶部と、前記論理式集合記憶部から選択した1つ以上の前記論理式の集合である候補条件を前記必須条件と共通要素を持つように生成する候補条件生成部10と、前記候補条件の論理積が成り立つときに前記プログラムが実行された直後に前記事後条件が成立するという命題が成立するか否かを判定する第1の判定部と、前記命題が成立すると決定された前記候補条件の論理積を、前記プログラムの事前条件として出力する出力部21と、を備える。【選択図】図1

請求項（抜粋）：

命令型プログラミング言語によって記述されたプログラムを記憶するプログラム記憶部と、 1つ以上の論理式の論理積である、前記プログラムの事後条件を記憶する事後条件記憶部と、 前記事後条件が成立するために前記プログラムの実行直前において少なくともその要素の一つが満たされる必要のある、1つ以上の論理式の集合である必須条件を複数記憶する必須条件記憶部と、 複数の論理式を記憶する論理式集合記憶部と、 前記論理式集合記憶部から選択した1つ以上の前記論理式の論理積である候補条件を前記必須条件との共通要素を持つように生成する候補条件生成部と、 前記候補条件の論理積が成り立つときに前記プログラムが実行された直後に前記事後条件が成立するという命題が成立するか否かを、前記命題の反例が存在するか否かを検査することにより判定し、前記命題の反例が存在しないとき前記命題が成立し、前記命題の反例が存在するとき前記命題が成立しないことを決定する第1の判定部と、 前記命題が成立すると決定された前記候補条件の論理積を、前記プログラムの事前条件として出力する出力部と、 を備えた事前条件生成装置。

IPC (1件)：

G06F 11/36

FI (1件)：

G06F9/06 620M

Fターム (2件)：

5B376BC64 ,  5B376BC69

引用文献：

出願人引用 (4件)

• Daikonの限定利用によるJavaメソッドの事後条件の自動導出
• システムレベル設計記述に対する具体値・記号値シミュレーションによる入力パターンの自動生成手法
• The Daikon system for dynamic detection of likely invariants
• Dynamically discovering likely program invariants to support program evolution