特許
J-GLOBAL ID:201703016923683994

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

発明者:
出願人/特許権者:
代理人 (1件): 特許業務法人サンクレスト国際特許事務所
公報種別:公開公報
出願番号(国際出願番号):特願2016-017419
公開番号(公開出願番号):特開2017-138677
出願日: 2016年02月01日
公開日(公表日): 2017年08月10日
要約:
【課題】不変条件を生成するための新たな技術を提供する。【解決手段】不変条件生成装置100は、プログラムコードが記憶される記憶部300と、不変条件を生成する処理を実行する処理部200を備える。処理部200は、多項式を構成するための1又は複数の部分式を生成する第2処理を実行する。第2処理は、指定部分式を取得する取得処理と、指定部分式に基づいて、多項式を構成するための1又は複数の部分式を生成する生成処理と、を含む。部分式は、プログラムコードに含まれるシンボルから構成可能な式である。生成処理は、プログラムコードの解析によって指定部分式との関連性が確認された1又は複数の関連部分式を、多項式を構成するための1又は複数の前記部分式として生成する。【選択図】図1
請求項(抜粋):
不変条件生成装置であって、 プログラムコードが記憶される記憶部と、 前記不変条件を生成する処理を実行する処理部を備え、 前記処理は、 前記記憶部から前記プログラムコードを読み出す第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ターム (5件):
5B042HH10 ,  5B042HH39 ,  5B042HH42 ,  5B376BC38 ,  5B376BC69
引用特許:
出願人引用 (2件)
引用文献:
出願人引用 (1件)
  • Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation

前のページに戻る