不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法

Inventor： , ,
Applicant, Patent owner：
Agent (1)：特許業務法人サンクレスト国際特許事務所
Gazette classification：公開公報
Application number (International application number)：2016017419
Publication number (International publication number)：2017138677
Application date： Feb. 01, 2016
Publication date： Aug. 10, 2017
Summary：

【課題】不変条件を生成するための新たな技術を提供する。【解決手段】不変条件生成装置100は、プログラムコードが記憶される記憶部300と、不変条件を生成する処理を実行する処理部200を備える。処理部200は、多項式を構成するための1又は複数の部分式を生成する第2処理を実行する。第2処理は、指定部分式を取得する取得処理と、指定部分式に基づいて、多項式を構成するための1又は複数の部分式を生成する生成処理と、を含む。部分式は、プログラムコードに含まれるシンボルから構成可能な式である。生成処理は、プログラムコードの解析によって指定部分式との関連性が確認された1又は複数の関連部分式を、多項式を構成するための1又は複数の前記部分式として生成する。【選択図】図1

Claim (excerpt)：

不変条件生成装置であって、プログラムコードが記憶される記憶部と、前記不変条件を生成する処理を実行する処理部を備え、前記処理は、前記記憶部から前記プログラムコードを読み出す第1処理と、多項式を構成するための1又は複数の部分式を生成する第2処理と、前記不変条件を生成する第3処理と、を含み、前記第2処理は、指定部分式を取得する取得処理と、前記指定部分式に基づいて、前記多項式を構成するための1又は複数の前記部分式を生成する生成処理と、を含み、前記部分式は、前記プログラムコードに含まれるシンボルから構成可能な式であり、前記生成処理は、前記プログラムコードの解析によって前記指定部分式との関連性が確認された1又は複数の関連部分式を、前記多項式を構成するための1又は複数の前記部分式として生成する不変条件生成装置。

IPC (2)：

G06F 11/36 , G06F 11/28

FI (2)：

G06F9/06 620P , G06F11/28 340A

F-Term (5)：

5B042HH10 , 5B042HH39 , 5B042HH42 , 5B376BC38 , 5B376BC69

Patent cited by the Patent：

Cited by applicant (2)

ソフトウェア仕様の証明支援装置、及び証明支援方法
Gazette classification：公開公報 Application number：特願2010-113811 Applicant：株式会社日立製作所
カバレージ測定装置
Gazette classification：公開公報 Application number：特願2008-317023 Applicant：トヨタ自動車株式会社

Article cited by the Patent：

Cited by applicant (1)

Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation

Return to Previous Page