Top > Search of Japanese Patents > INVARIANT GENERATOR, COMPUTER PROGRAM, INVARIANT GENERATING METHOD, AND PROGRAM CODE PRODUCING METHOD

INVARIANT GENERATOR, COMPUTER PROGRAM, INVARIANT GENERATING METHOD, AND PROGRAM CODE PRODUCING METHOD meetings

Patent code P200016748
File No. 5207
Posted date Apr 8, 2020
Application number P2016-017419
Publication number P2017-138677A
Patent number P6622098
Date of filing Feb 1, 2016
Date of publication of application Aug 10, 2017
Date of registration Nov 29, 2019
Inventor
  • (In Japanese)末永 幸平
  • (In Japanese)樹下 稔
  • (In Japanese)小島 健介
Applicant
  • (In Japanese)国立大学法人京都大学
Title INVARIANT GENERATOR, COMPUTER PROGRAM, INVARIANT GENERATING METHOD, AND PROGRAM CODE PRODUCING METHOD meetings
Abstract PROBLEM TO BE SOLVED: To provide a novel technique for generating invariants.
SOLUTION: An invariant generator 100 includes a storage unit 300 having a program code stored therein, and a processing unit 200 for executing invariant generation processing. The processing unit 200 executes a second process for generating one or more sub-expressions for building a polynomial. The second process includes an acquisition process for acquiring a specified sub-expression, and a generation process for generating one or more sub-expressions for building a polynomial based on the specified sub-expression. The sub-expressions are expressions that can be built from symbols included in a program code. The generation process generates one or more related sub-expressions confirmed to be related to the specified sub-expression by a program code analysis as the one or more sub-expressions for building a polynomial.
Outline of related art and contending technology (In Japanese)

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

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

Field of industrial application (In Japanese)

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

Scope of claims (In Japanese)
【請求項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(International Patent Classification)
F-term
Drawing

※Click image to enlarge.

JP2016017419thum.jpg
State of application right Registered
Please contact us by e-mail or facsimile if you have any interests on this patent. Thanks.


PAGE TOP

close
close
close
close
close
close
close