TOP > 国内特許検索 > 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法

不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法 UPDATE 新技術説明会

国内特許コード P200016748
整理番号 5207
掲載日 2020年4月8日
出願番号 特願2016-017419
公開番号 特開2017-138677
登録番号 特許第6622098号
出願日 平成28年2月1日(2016.2.1)
公開日 平成29年8月10日(2017.8.10)
登録日 令和元年11月29日(2019.11.29)
発明者
  • 末永 幸平
  • 樹下 稔
  • 小島 健介
出願人
  • 国立大学法人京都大学
発明の名称 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法 UPDATE 新技術説明会
発明の概要 【課題】不変条件を生成するための新たな技術を提供する。
【解決手段】不変条件生成装置100は、プログラムコードが記憶される記憶部300と、不変条件を生成する処理を実行する処理部200を備える。処理部200は、多項式を構成するための1又は複数の部分式を生成する第2処理を実行する。第2処理は、指定部分式を取得する取得処理と、指定部分式に基づいて、多項式を構成するための1又は複数の部分式を生成する生成処理と、を含む。部分式は、プログラムコードに含まれるシンボルから構成可能な式である。生成処理は、プログラムコードの解析によって指定部分式との関連性が確認された1又は複数の関連部分式を、多項式を構成するための1又は複数の前記部分式として生成する。
【選択図】図1
従来技術、競合技術の概要

不変条件(Invariant)は、プログラムコード(以下、単に「コード」ということがある)の形式的検証(formal verification)に用いられる。形式的検証は、プログラムコードの正当性を数学的な形式的手法で証明することである。プログラムコードに含まれるある処理に対する不変条件は、その処理の実行前後において成立する条件として構成される。while文のようなループ処理に対する不変条件は、ループ不変条件(Loop Invariant)と呼ばれる。ループ不変条件は、ループの開始時点で成立するとともに、ループを何回繰り返しても成立する条件として構成される。

不変条件を生成する従来の方法には、非特許文献1等に記載のテンプレート法(template-based method)がある。テンプレート法では、多項式pが、不変条件に関係する多項式のテンプレートとして生成される。多項式pは、検証対象のプログラムコードに含まれるシンボルと不定係数によって構成される。シンボルとは、プログラムに含まれる変数又は定数を示す文字又は記号である。そして、p=0が不変条件であるような制約が生成される。この制約を解析することで、不変条件が得られる。

産業上の利用分野

本発明は、不変条件生成装置等に関するものである。

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

【請求項2】
前記プログラムコードに基づく前記解析は、
前記プログラムコードに含まれる前記シンボルの次元型解析によって、複数の前記シンボルそれぞれの次元型を求めること、
前記指定部分式の次元型を求めること、
を含み、
前記関連部分式は、前記シンボルから構成可能な部分式のうち、前記指定部分式の次元型と一致する次元型を有することが確認された部分式である
請求項1記載の不変条件生成装置。

【請求項3】
前記第2処理は、指定次数を取得することを更に含み
前記関連部分式は、前記指定次数以下の次数の部分式である
請求項2記載の不変条件生成装置。

【請求項4】
前記プログラムコードに基づく前記解析は、
前記指定部分式だけを要素として有する前記部分式の初期集合Bを生成すること、
前記指定部分式を変数qの初期値とすること、
φ(q)が、前記集合Bに含まれる1又は複数の前記部分式の線形結合として表現される式になることが確認されるまで、後述の第1更新ステップ及び第2更新ステップを含む繰り返し処理を実行すること、
を含み、
前記関連部分式は、前記繰り返し処理が終了したときに、前記集合Bに含まれる1又は複数の部分式であり、
前記φ(q)は、変数qが示す式を、前記プログラムコードに従って変化させる関数であり、前記プログラムコードに基づいて求められ、
第1更新ステップは、前記集合Bの要素に前記φ(q)を加えるステップであり、
第2更新ステップは、前記φ(q)を新たなqとするステップである
請求項1記載の不変条件生成装置。

【請求項5】
請求項1~4のいずれか1項に記載の不変条件生成装置としてコンピュータを機能させるためのコンピュータプログラム。

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

【請求項7】
プログラムコードを作成すること、
請求項6に記載の前記記憶部が、作成されたプログラムコードを記憶すること、
請求項6に記載の方法によって、前記プログラムコードの不変条件を生成すること、
前記不変条件を用いて、前記プログラムコードの形式的検証を行うこと、
前記形式的検証の結果に基づいて前記プログラムコードを修正すること、
を含むプログラムコードの製造方法。
国際特許分類(IPC)
Fターム
画像

※ 画像をクリックすると拡大します。

JP2016017419thum.jpg
出願権利状態 登録
ライセンスをご希望の方、特許の内容に興味を持たれた方は、下記までご連絡ください。


PAGE TOP

close
close
close
close
close
close
close