日本ソフトウェア科学会第 34 回大会 (2017 年度) 講演論文集

データ駆動アプローチによるプログラムの線形写像化
石澤 拓哉

小島 健介

末永 幸平

本論文ではプログラムの線形写像表現を計算するアルゴリズムを提案する，プログラム c について，線形写像 Aがプログラム c の線形写像表現であるとは，ベクトル ⃗x で表された任意のプログラムの状態について，⃗
x を初期状態として c を実行して停止するならば終了状態が A⃗
x となることをいう．線形写像表現はプログラム検証やプログラ
ムの最適化のために有用である．提案アルゴリズムは以下の操作を繰り返し行うことで線形写像表現を計算する．まずプログラム c の線形写像表現として全ての要素が未定係数である行列 T を生成する．次にテストとなる状態を生成し，そのテストを初期状態として c を実行した結果から T の未定係数を決定する．求めた T が正しい線形写像となるかを外部のソルバを用いて検証する．検証に成功すれば T を出力し，失敗すればソルバが返す反例をテストに加える．本論文では提案アルゴリズムが停止性，健全性，完全性を満たすことを証明する．

We propose an algorithm to compute a linear-mapping representation (LMR) of a program. Given a program c, an LMR of c is a matrix A such that A⃗
x is identical to the result of executing c with the state
expressed as a vector ⃗x. Such representation is useful in program verification and program optimization.
Our algorithm computes an LMR of program c by iterating the following steps. First, the algorithm designates a template T of an LMR of c. T is a matrix elements of which are unknowns. Then, the algorithm
randomly generates and executes a test to determine the unknowns in T . The algorithm then tries to verify
that the estimated matrix is a correct LMR of c using an external solver. If the verification fails and thesolver returns a counterexample, the algorithm adds it to the set of tests that are used in the next iteration.
We show the soundness, the completeness and the convergence of our algorithm.

ことである．

1 はじめに
静的検証はプログラムがあらかじめ定められた性
質を満たすことをプログラムの実行前に証明する手

例 1.1. 以下のプログラム
x := N ; sum := 0

while x ̸= 0 do法である．様々な静的検証手法が研究されており，近(x, sum) := (x − 1, sum + x)

年は実用に供されている手法も多く存在する [1, 4, 6]．

end
において，N ≥ 0 であれば，1 から x までの総和

ループを含む命令型プログラムの静的検証においては良いループ不変条件を発見することが重要である [15]．ループ不変条件とは，プログラムの制御がループの先頭に到達したときに必ず成り立つ条件のComputing Linear-Mapping Representations of Programs by Data-Driven Approach
Takuya Ishizawa, 京都大学, Kyoto University.
Kensuke Kojima, 京都大学 / JST CREST, Kyoto University / JST CREST.
Kohei Suenaga, 京都大学 / JST PRESTO, Kyoto University / JST PRESTO.

と sum の値の和はループの先頭に制御が到達した
時点では必ず 1 から N までの総和に等しいので，
x(x+1)+ sum − N (N2+1) = 0 はループ不変条件であ2

る．このループ不変条件を使えば，ループを抜けたときに x = 0 であることと併せて，プログラム終了時
点で sum = N (N2+1) であることが証明できる．
ループ不変条件を自動的に発見する手法は，プログ
ラム検証の研究において重要なテーマであり，保証したい性質に応じて様々な手法がこれまでに提案されている．特にプログラム中に現れる変数 x1 , . . . , xn の多項式 p(x1 , . . . , xn ) を用いて p(x1 , . . . , xn ) = 0 の形に書けるループ不変条件（代数的不変条件）の発見手法は近年においても多くの手法が提案されている [2, 3, 9–14] ．

De Oliveira らは代数的不変条件の発見手法として

きる．





x
1
0 0 −1
x







 sum 
 1
1 0
0 



  sum  7→ 

2
2


 x 
 −2 0 1
1 
 x 



1
1
0
0 0
1
この行列の転置行列の固有値 1 の固有ベクトルはす

行列 Ac′ を計算し，Ac′ の転置行列 Ac′ t の固有ベク
トルからループ不変条件を求める手法である．†1

べて以下の３つのベクトルの線形結合として書ける．

 
 

1
0
0

 
 

 0   0   2 

 
 


,
,

 0   0   1 
 


 
0
0
1
このうち３つ目のベクトル (1, 2, 1, 0)t と算術式の固有ベクトル法においては，算術式のベクトル B

ベクトル (x, sum, x2 , 1) との要素ごとの積の和はをユーザが入力として与え，その算術式の値がループ

x + 2sum + x2 となり，この式の値はループ本体一回

本体の一回の実行でどのように変化するかを線形写像の実行では変化しない．このループの先頭に初めてで表現する．ループ本体の一回の実行が線形写像 A

制御が到達したときのこの式の値は N + N 2 なので，を用いて B 7→ AB と書けるとして，A の転置行列 A

x + 2sum + x2 = N + N 2 はループ不変条件である．

に固有値 1 の固有ベクトル ⃗c があったとしよう．このときに ⃗c と B の要素ごとの積の和 †2⃗ct B の値はルー固有ベクトル法は代数的不変条件を生成する有力な手法であるが，ネストしたループを含むプログラム

プ一回の実行で変化しない．実際にループ一回の実行には適用できないという欠点がある．

によって算術式 ⃗ct B の値は ⃗ct AB に変化するが，⃗ct A

例 1.3. 以下のプログラムは，例 1.1 のループ本体を固有ベクトル法と呼ばれる手法を提案した [7]．この手法はループ文 while b do c′ のループ不変条件を求めるために，c′ の実行を表現した線形写像の表現ttは (At⃗c) に等しく，固有ベクトルの定義から At⃗c は⃗c に等しいため，⃗ct AB の値は ⃗ct B に等しい．従って，初めにこのループの先頭に制御が到達したときの ⃗ct B

t

さらにループ文を用いて書いたプログラムである．
x := N ; y := 0; sum := 0;

while x ̸= 0 doの値を p とすれば，⃗c B − p = 0 はループ不変条件とy := x;なっている．

while y ̸= 0 do · · · · · · (∗)

t

例 1.2. 例 1.1 のプログラムを用いて固有ベクトル法
2(y, sum) := (y − 1, sum + 1);

を説明する．ここでは算術式の組として (x, sum, x , 1)

end

が 与 え ら れ た と し よ う．ル ー プ 本 体 の コ マ ン ド

x := x − 1;(x, sum) := (x − 1, sum + x) の実行によって，それぞれの算術式は (x − 1, sum + x, x − 2x + 1, 1) に
2変化する．この算術式の変化は，算術式の組をベクトルと見れば，以下の線形写像として表現することがで†1 以下では「線形写像」という語をその表現行列を指すために用いることがある．
†2 B が算術式のベクトルなので，この要素ごとの積の和は算術式である．

end
このプログラムは例 1.1 のプログラムと同じ意味を持つが，ネストしたループを含むために固有ベクトル法を適用することができない．
固有ベクトル法をネストしたループを含むプログ
ラムに拡張するにあたっての困難は，ループ文自体の動作を表現する線形写像の計算にある．例えば例 1.3のプログラムに固有ベクトル法を適用するためには，(∗) で示した内側のループ文の実行を線形写像で表現する必要がある．この写像が (y, sum) 7→ (0, y) であることを計算するのは必ずしも自明ではない．
本論文では，ネストしたループを含むプログラムに固有ベクトル法を拡張することを目指して，与えられ例えば，状態 {x 7→ 1, y 7→ 2, z 7→ 3} は x < y < z とたプログラムの線形写像表現を求める手法を提案す

順序を仮定することで，(1, 2, 3)t と表せる．以降ではる．提案手法を用いることで，例 1.3 のようなプログ

部分関数としての状態とベクトルとしての状態を区ラムにおいてもループ本体の動作を線形写像として表別しない．

現することができ，固有ベクトル法を拡張することが基底は単項式のベクトル，すなわち Mn の要素で可能になると期待される．
（但し，本論文においてはある．基底 B ∈ M 中の各単項式を状態 σ に従ってプログラムの動作の線形写像表現を求める手法のみを評価した Rn の要素を JBKσ と書く．例えば，基底 B扱い，固有ベクトル法の拡張にまでは踏み込まない．
）

を (x, y, x2 , xy, 1) とおき，順序 x < y のもとで状態提案手法の特徴は，与えられたプログラムの線形写

σ を (2, 3)t とおくと，JBKσ = (2, 3, 4, 6, 1)t となる．

t

像表現をデータ駆動アプローチを用いて求める点にある．ここでデータ駆動アプローチとは，プログラム

2. 2 対象言語に対するテストを自動生成し，そのテストの実行結果

以下の言語を対象とする．
c ::= skipから線形写像表現を推測する手法である．線形写像表
現の推測後に，推測された表現が正しいことを検証す| (x1 , ..., xn ) : =(p1 , ..., pn )るフェーズを設けることで，正しい線形写像表現が計| c1 ; c2

算されることを保証する．また，この検証が失敗した| if b then c1 else c2

際に，検証過程で生じた反例をテストとして用いるこ| while b do c endとで，線形写像表現を決定するのに必要なテストをシ
ステマティックに生成することができる．
本論文では与えられたプログラムの線形写像表現
を計算するアルゴリズムを提案し，その正しさを証明する．アルゴリズムの実装と評価，並びに固有ベクトル法の拡張は今後の課題である．
本論文の構成を説明する．2 節では論文中で使用する定義を導入する．3 節におけるアルゴリズムの説明
では，まず 3. 1 節において動作例を用いてアルゴリズ
ムの直観的な説明を行った後に，3. 2 節でフォーマルな定義を述べる．4 節ではアルゴリズムの停止性，健全性，完全性を示す．5 節で関連研究を論じた後に，

6 節で結論と今後の課題を述べる．

2 準備
2. 1 定義
PV をプログラム変数の集合，M をプログラム変数上の単項式全体の集合とする．PV の要素を表すためにメタ変数 x, y, z, . . . を用いる．(−)t はベクトルもしくは行列の転置を表す．
状態とは PV から R への部分関数である．メタ変
数 σ で状態を表す．本論文ではプログラム変数間に暗黙に全順序をつけることで状態をベクトルとして扱う．

| assume b
ここで，x はプログラム変数，b はブール式，p はプ
ログラム変数上の多項式を表す．

skip は 空 文 を 表 し ，状 態 を 変 化 さ せ な い ．
(x1 , ..., xn ) : =(p1 , ..., pn ) は，1 ≤ i ≤ n に対して，
xi に pi の評価結果を全て同時に代入する操作である．c1 : = c2 は c1 を実行した直後に c2 を実行する操作である．if b then c1 else c2 は b を評価して true
ならば c1 を実行し，false ならば c2 を実行する操作である．while b do c end は b が false になるまで cを繰り返し実行する操作である．assume b は実行時に b が true ならば何もせず，false ならば無限ルー
プする．

JcKσ は，プログラム c を初期状態 σ で実行し，停止した時の終了状態を表す．停止しない時は結果は ⊥という特別な値になるものとする．
プログラム c の基底 B における線形写像表現（あるいは単に c の線形写像表現）とは，任意の状態 σ について，JcKσ ̸= ⊥ ならば JBKJcKσ = AJBKσ となる線
形写像 A のことである．また，プログラム c を線形写像表現に変換することを線形写像化と呼ぶ．例えば，プログラム c が以下のように与えられたとする．
assume x > 0

while x ̸= 0 do

案する．提案アルゴリズムの入力と出力は以下の通り
である．
入力 プログラム c，基底 B，アサーション φ．

(x, y) : =(x − 1, y + 1)

出力 c の事前条件が φ であると仮定したときの cend(x, y, 1)t 7→
基底 B を (x, y, 1)t とすると，c の動作は

0



(0, x + y, 1)t と表現できる．このとき，
 x+y 
1



0 0 0
x






は  1 1 0  y 
 と表現できる．したがっ
0 0 1
1


0 0 0


t

て
 1 1 0  は基底 (x, y, 1) における c の線形0 0 1
写像表現である．

の B 上での線形写像表現，もしくはアルゴリズの線形写像表現をデータ駆動アプローチ，すなわち，提案するアルゴリズムにおいてはホーア論理においする前に，以下のプログラム csum についてこのアルて導入される概念を用いる．以下では本論文で必要となる概念を，正確な定義を述べること無しに，簡潔に説明する．詳細な説明は Winskel による教科書 [15]を参照されたい．
アサーションとは PV の要素を自由変数として含みうる実数の上の一階述語論理式のことである．アサーションをメタ変数 P または Q で表す．アサーション P 中の自由変数の値を状態 σ に従って解釈す
ると P が成り立つとき σ |= P と書く．任意のアサームが失敗したことを示す fail．

3. 1 アルゴリズムの動作例
GuessAndCheck の特徴は，与えられたプログラム与えられたプログラムの初期状態を生成し，その実行
結果から線形写像表現を求める点である．このアプローチは 5 節で議論する Sharma ら [11, 14] の手法に着想を得ている．
この節では，GuessAndCheck をフォーマルに定義
ゴリズムがどう動作するかを説明する．
assume x > 0

while x ̸= 0 do(x, sum) : =(x − 1, sum + x)
end
GuessAndCheck は プ ロ グ ラ ム csum の 他 に 基 底
B を 入 力 と し て 受 け 取 る ．†3 こ こ で は B と し てt(x, sum, x2 , 1) を与えたとしよう．csum の動作はtt

写像 (x, sum, x2 , 1) 7→ (0, sum + 21 (x + x2 ), 0, 1)

直観的には {P }c{Q} は条件 P を満たす状態からプロで表現できる．また，この写像のB 上の線形写像

0 0 0 0
 1 1 1 0 
 2

2
表現は 
 である．アルゴリズム
 0 0 0 0 
0 0 0 1
GuessAndCheck はデータ駆動アプローチを用いてこ

グラム c を実行して停止すれば，条件 Q を満たすといの線形写像表現を求める．

ション P に対して，⊥ |= P であると約束する．任意の σ について σ |= P であるとき，|= P と書く．
プ ロ グ ラ ム c と ア サ ー ション P, Q に つ い て ，{P }c{Q} をホーア三つ組と呼ぶ．ホーア三つ組はう意味である．具体的には，σ |= P ならば JcKσ |= Q

GuessAndCheck はテスト σ とテンプレート行列であるときにホーア三つ組 {P }c{Q} が成り立つと言T := (tij )1≤i,j≤|B| を生成する．テストはプログラム

い，|= {P }c{Q} と書く．ホーア三つ組 {P }c{Q} のの開始状態を表すベクトルであり，ランダムに生成すればよい．†4 テンプレート行列は行列の各要素が未定

P を c の事前条件，Q を c の事後条件と呼ぶ．

3 アルゴリズム
この節ではプログラム c を与えられたときに，c を線形写像化するアルゴリズム GuessAndCheck を提†3 この節では説明の簡単のために，プログラムの事前条
件をとして与えられるアサーション φ のことは考えない．
†4 後に示す GuessAndCheck の定義においては，プロ
グラム c が満たすべき事前条件を考慮に入れてテストを生成するようになっている．

係数である行列であり，GuessAndCheck は生成されもし C が成り立たない場合は，C の反例となる ⃗a がたテストの実行結果からテンプレート行列中の未定存在するはずなので，⃗a をテスト，T をテンプレート

係数の間の制約を生成し，その制約の解から線形写像

行列として，再びアルゴリズムを動作させる．なお，化を徐々に求める．

求まった行列が正しい線形写像表現になっているかどtt

テ ス ト と し て (x, sum) 上 の 状 態 σ1 := (1, 0)

うかの検証の際に，テンプレート行列 T を用いずにが 生 成 さ れ た と し よ う．GuessAndCheck は 終 了状 態 Jc
K を 求 め る ．†5 こ こ で は 終 了 状 態 はインスタンス化された行列 T ′ を用いても，最終的にJcsum Kσ1 = (0, 1)t となる．

理 4.3 で述べる．

sum σ1

T が csum の線形写像表現であるためには，csum が停止する任意の状態 σ について，JBKJcsum Kσ = T JBKσが成り立つ必要がある．この制約は，テンプレート行
列中の未定係数の間の連立一次方程式に帰着できるので，SMT ソルバ等を用いて容易に解くことができる．

σ を上記の σ1 としてこの制約を解き，その解をTにt11 t12 t13−t11 − t13



 t
 21 t22 t23 1 − t21 − t23 
代入すると T =  t31 t32 t33−t31 − t33 
t41 t42 t43 1 − t41 − t43となる．
次にここで求めた T が csum の線形写像表現になっているかどうかを検証する．これには，任意の状態 ⃗aと任意の tij で |= {B = JBK⃗a }csum {B = T JBK⃗a } が成り立つかをプログラム検証器や SMT ソルバを用いて調べればよい．しかし，T 中に未解決の未定係数が多く存在するために，これらのソフトウェアを用いてこの三つ組の成否を判定することは多くの場合難しい．
そ こ で GuessAndCheck で は ，T 中 に 残 る 未 定′

係数に 0 を代入して得られる行列 T （この行
列 を イ ン ス タ ン ス 化 さ れ た 行 列と 呼 ぶ ）が 条 件|= {B = JBK⃗a }csum {B = T ′ JBK⃗a } を満たすかどうかを検証する．†6 この条件を以下で C と呼ぶ．もしT ′ が条件 C を満たすならば，T ′ は csum の正しい線形写像表現になっているので，T ′ を出力すればよい．
†5 実際には csum が σ1 を初期状態にとると停止しない
場合も考えられるので，あらかじめ定めた実行ステッ
プ数を超えても csum が停止しない場合は，アルゴリ
ズム自体を異常終了することにする．
†6 テンプレート行列をインスタンス化する際に未定係数に代入する値は任意の値でよく，0 でなくともアルゴ
リズムの正しさには影響はない．ここでは簡単のために 0 を代入するものとして説明する．

は線形写像表現が（存在するならば）求まることを定




0


 0

この例では T = 
 0


0

0

0

0

0


1 

 は csum の動
0 0 0 
0 0 0 1
作を正しく表してはいない．なぜならば，σ2 := (2, 0)t′とすれば，Jcsum Kσ2 := (0, 3)t となり，JBKJcsum Kσ2 =T ′ JBKσ2 を満たさないからである．よって，反例 σ2をテスト，テンプレート行列を T として再びアルゴ
リズムを動作させる．
始めの反復と同様に制約 JBKJcsum Kσ2 = T JBKσ2


−3t13
t12 t132t13
 2 − 3t
t22 t23 −1 + 2t23 23
を解くと T =  −3t33

t
t
2t
32
33
33


−3t43
t42 t43
1 + 2t43が解として得られる．このT のインスタンス化され


0 0 0
0


 2 0 0 −1 
た行列は T ′ =  となるが，これ
 0 0 0
0 


0 0 0
1
もまた csum の動作を正しく表してはいない．反例としては σ3 = (3, 0)t がとれる．よって，σ3 をテスト，テンプレート行列を T として再びアルゴリズムを動作させる．

 反 例 σ3
0 t12

 1 t
22
 2

 0 t32

0 t42

のもと
 で 制 約 を 解 く と ，T =
0 0

1
0 

2
 が解として得られる．インスタ
0 0 

0 0


0 0 0 0
1
 1 2 0 2 0 ′
ンス化された行列は T =  とな 0 0 0 0 
0 0 0 0るが，反例として σ4 = (1, 1)t が存在する．σ4 をテ

スト，T をテンプレート行列として再びアルゴリズム
0 0 0 0
 1 1 1 0 
 2
2を動作させ，制約を解くと T =  0 0 0 0 
0 0 0 1が得られる．T ′ は条件 C を満たすため，csum の動作
を正しく表している．よって，GuessAndCheck は T ′を出力する，この T ′ が csum の線形写像表現となる．

線形写像化できないプログラムであっても，事前条件を限定することで線形写像化できる場合があり，条件 φ によってこのようなプログラムも扱えるようにする．†7
アルゴリズム 1 中では以下の補助的な手続きを用いている．

• Choose
集合を入力としてその集合の要素を任意に一つ選んで返す手続き．

3. 2 アルゴリズム GuessAndCheck• GenTest
アサーション φ を入力として φ を満たす状態を

input : プログラム c，基底 B，アサーション φ
output: c の B 上での線形写像表現|B|×|B|

任意に一つ返す手続き．

• Executeプログラム c と状態 σ を入力として，c を入力

1

T ←R

2

σ ← GenTest B (φ);σ のもとで実行した後の状態 JcKσ を返す手続き．

3

while true do

事前に設定した計算ステップ数を超えても c が停

4;止しなければ，例外 timeout を発生させる．

′

try σ ← Execute(c, σ) with

以下ではアルゴリズム 1 中で重要な箇所について

timeout → fail;5

T ← {T ∈ T | JBKJcKσ = T JBKσ };6

if T ′ = ∅ then9

• 3. 1 節の説明においてはテンプレート行列 T を用いて線形写像表現を求めたが，アルゴリズム 1

fail;

7
8

説明する．

′

中ではテンプレート行列を明示的には扱わず，代end

わりにテンプレート行列のインスタンスの集合′

T ←T ;10

T ← Choose B (T );T を扱っている．これは，4 節でのアルゴリズム

11

if ∀⃗a.φ[⃗a/⃗x] =⇒ |= {B = JBK⃗a }c{B =の性質の議論を簡潔にするためである．1 行目は

T ′ JBK⃗a } が恒真 then

3. 1 節のテンプレート行列の生成，5 行目はテン′

return T

121314

プレート行列 T について JBKJcKσ = T JBKσ を解′くことにそれぞれ対応している．

end′

σ を φ[σ/⃗x]∧ ̸|= {B = JBKσ }c{B = T JBKσ }を満たす状態とする．

• 11 行目においては ∀⃗a.φ[⃗a/⃗x]=⇒ |= {B =′JBK⃗a }c{B = T JBK⃗a } が恒真であるかを判定する

end必要がある．この条件が満たされれば，φ を満た

Algorithm 1: アルゴリズム GuessAndCheck ．

す状態については，T ′ は c の線形写像表現にな

15

る．この判定には SMT ソルバ [6] を用いること

GuessAndCheck の定義をアルゴリズム 1 に示す．
このアルゴリズムはプログラム c と基底 B とアサーション φ を入力とし，c の B 上での線形写像表現を出力する．条件 φ は c の事前条件である．条件 φ はGuessAndCheck 中で事前条件を満たすテストのみが生成されるようにするために用いられる．一般にはを想定している．

4 性質
この章では 3 章で示したアルゴリズム

GuessAndCheck の性質を示す．補題の証明は付録 A†7 実際に 3. 1 節の動作例においては，事前条件 x > 0を考慮しなければ線形写像化することができない．

が空集合となり fail する．

に述べる．

4. 2 健全性

4. 1 停止性
定理 4.1 (停止性). GuessAndCheck は任意の入力に定理 4.2 (健全性). 任意のプログラム c，基底 B ，事対して停止して線形写像表現を返すか fail する．

前条件 φ について，T := GuessAndCheck (c, B, φ)

これを示すためにいくつかの補題を示す．

が fail でなかったとする．任意の状態 ⃗a について

定義 4.1. ベクトル空間 V の空でない部分集合 A
が aﬃne subspece であるとは，ある a ∈ A について

A − a = {b − a|a ∈ A} が V の線形部分空間となることである．

φ[⃗a/⃗x] =⇒ {B = JBK⃗a }c{B = T JBK⃗a } が成り立つ．
(証明) GuessAndCheck (c, B, φ) が fail 以外を返すのは 11 行目の検証条件が真となった場合のみである
ことから明らか．

Aﬃne subspace の次元を以下のように定義する．
定義 4.2. A が aﬃne subspace のとき，a ∈ A について dim(A − a) を aﬃne subspace の次元と言い，

dim A と書く．
以 下 の 補 題 は ，aﬃne subspace の 次 元 が well-defined であることを保証する．
補題 4.1. A がベクトル空間 V の aﬃne subspace のとき，A − a は a ∈ A の取り方によらず同じ集合となる．
以下の補題は，Algorithm 1 の 5 において T ′ が必
ず aﬃne subspace になることを保証する．
補題 4.2. A が行列の成す線形空間 Rm×n の aﬃnesubspace であるとき，u ∈ Rm , v ∈ Rn について
A′u,v := {T ∈ A|u = T v} が空でないとする．このとき，A′u,v は Rm×n の aﬃne subspace である．
補題 4.3. A, B が aﬃne subspace で，B ⊆ A とする．このとき dim B ≤ dim A となる．また，等号が成り立つのは A = B のときに限る．
補 題 4.4. 任 意 の 基 底 B と aﬃne subspace T ⊆4. 3 完全性
定 理 4.3 (完 全 性). プ ロ グ ラ ム c が 任 意 の
初 期 状 態 に つ い て 停 止 す る と 仮 定 し ，S

{T

∈

R

|B|×|B||∀⃗a.φ[⃗a/⃗
x]

=⇒

|=

{B

:=
=

JBK⃗a }c{B = T JBK⃗a }} とする．S が空でなければ，
GuessAndCheck (c, B, φ) は S の元を返す．
定理 4.3 は，プログラム c がすべての初期状態について停止することを要求する．状態 σ を初期状態とすると c が停止しない場合において，GenTest がσ を生成すると，4 行目でアルゴリズムが失敗するた
め，実際には c の線形写像表現が存在する場合においても，それを返すことができないためである．
補 題 4.5. S を 定 理 4.3 中 の と お り に 定 義 す る ．

T0′ := R|B|×|B| とし，n 回目にアルゴリズム 1 中の 5 行目が実行されたときの T ′ の値を Tn′ と書く．
任意の n で S ⊆ Tn′ ．

(証明) (定理 4.3) 補題 4.5 より，5 行目において必と T ∈ T について，σ を φ[σ/⃗x]∧ ̸|= {B =ず S ⊆ T ′ となり，S が空でないとき，T ′ も空でな

JBKσ }c{B = T ′ JBKσ } を満たす任意の状態ベクトルとい（すなわちアルゴリズムは fail を返さない．
）よっR|B|×|B|′

する．ここで，T ′ := {T ∈ T |JBKJcKσ = T JBKσ } と
おくと，T ′ ⊊ T ．

(証明) (定理 4.1) 補題 4.4 より，Algorithm 1 の 5 行
目の T ′ はループを実行するたびに真に小さくなるこて定理 4.1 より，GuessAndCheck は線形写像 T ′ を出力する．検証条件より T ′ ∈ S となることは明らか．

5 関連研究とが分かる．これと補題 4.3 より，aﬃne subspace T ′本論文で提案したアルゴリズムは Sharma ら [14]の次元がループのたびに真に小さくなることが分かの手法に着想を得ている．彼らはプログラムの実行か

2

る．T の次元は最大で |B| なので，GuessAndCheckら得られるデータから不変条件を推測し検証する手は高々|B|2 回の反復で線形写像表現を出力するか，T ′法を提案した．彼らは後に基底を自動的に求めながら′プログラムの事前条件を計算するアルゴリズムも提案している [11]．本論文ではデータ駆動アプローチを

6 結論

プログラムの線形写像化の問題に適用した．彼らの手本論文ではデータ駆動アプローチを用いてプログ

法との主な差分は，線形化の候補が正しいことの検証

ラムの線形写像表現を求めるアルゴリズムを提案しを行う際の効率を向上するために，我々の手法では推た．提案した手法では，プログラムの初期状態を順次定された線形写像に残存する未定係数に 0 を代入し生成し，生成された状態から始めてプログラムを実行た上で検証を行う点である．これがアルゴリズムのして終了状態を計算し，初期状態と終了状態の間の関停止性と完全性を損なわないことが保証されている．

係から線形写像表現の候補を求める．求められた候

彼らの基底の自動生成へのアプローチの我々の手法へ補が正しい線形写像表現になっているかどうかをプの適用は重要な将来の課題である．

ログラム検証器で検証し，もし正しくないという結Sharma らの手法の他にも代数的不変条件を自動生果が得られた場合は，得られた反例を新たに初期状成する研究はここ十数年研究が進んでいる．これらの態として再び線形写像表現を求める．以上のループ研究は主に多項式代数を用いて代数的不変条件を生を繰り返すことで，停止するプログラムについては，成する．Sankaranarayanan ら [13] はグレブナー基

線形写像表現が存在するならば有限時間でそれが求底を用いて代数的不変条件を自動生成する手法を提まることを証明した．

案した．彼らのアルゴリズムは，ループ文の代数的不本アルゴリズムが正しく動作することを小さな例

変条件を与える多項式の集合のグレブナー基底を求で確認しているが，より大きなプログラムを用いた評めることで代数的不変条件を計算する．Müller-Olm

価はまだ行っていない．アルゴリズムを実装しベンチ

ら [10] は抽象解釈 [5] を用いた手法を提案している．

マークで評価することは重要な課題である．

Rodrı́guez-Carbonell ら [12] らはある限られたクラ提案手法が使う基底は，現在人手で与えることを仮スの命令型プログラムについては，任意のループ文

定しているが，もし与えられた基底が線形写像表現をの代数的不変条件の基底をなすグレブナー基底を求構成するために不十分であった場合は，提案するアルめる問題は決定可能であることを示した．Cachera

ゴリズムは失敗する．アルゴリズム 1 の 7 行目に到ら [2, 3] は代数的不変条件の計算をグレブナー基底を達した場合がこのケースに相当するが，この場合にこ用いずに行うアルゴリズムを提案した．彼らは未定

れまでに生成されたテストの集合を解析することで，係数を含むテンプレート多項式 p について，p = 0 が基底として足りない単項式を生成することができる

ループ不変条件となるための条件を多項式に対する場合がある．Sharma ら [11] の基底の自動生成アル演算でエンコードし，未定係数の間に成り立つべき制

ゴリズムは，実際にこのようにして新しい基底を学習

約を求め，それを解くことで代数的不変条件を求めしており，提案手法においても同様のアプローチが適る．小島ら [9] はテンプレート多項式に含まれる必要用できる可能性がある．

のない単項式を次元型 [8] を用いたプログラム解析で謝辞

求め，テンプレート多項式のサイズを小さくすること

小島は JST CREST の助成を，末永は JST さき

で，彼らの手法を高速化する方法を提案した．データ

がけ (No. JPMJPR15E5) と科研費 (15KT0012) の駆動アプローチを用いた手法は，多項式代数を用いた助成を受けて本研究を行った．

手法に比べて，多くの場合軽量であり，プログラムの
ソースコードが必ずしも無くても適用が可能である

参 考 文 献という利点がある．

[ 1 ] Beyer, D. and Keremoglu, M. E.: CPAchecker:
A Tool for Configurable Software Verification, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 1420, 2011. Proceedings, 2011, pp. 184–190.

[ 2 ] Cachera, D., Jensen, T., Jobin, A., and Kirchner, F.: Fast inference of polynomial invariants forimperative programs, Technical Report RR-7627,
INRIA, 2011.
[ 3 ] Cachera, D., Jensen, T. P., Jobin, A., and Kirchner, F.: Inference of polynomial invariants for imperative programs: A farewell to Gröbner bases,
Sci. Comput. Program., Vol. 93(2014), pp. 89–109.
[ 4 ] Calcagno, C., Distefano, D., Dubreil, J., Gabi,
D., Hooimeijer, P., Luca, M., O’Hearn, P. W., Papakonstantinou, I., Purbrick, J., and Rodriguez, D.:
Moving Fast with Software Verification, NASA Formal Methods - 7th International Symposium, NFM
2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings, 2015, pp. 3–11.
[ 5 ] Cousot, P. and Cousot, R.: Abstract Interpretation: A Unified Lattice Model for Static Analysis
of Programs by Construction or Approximation of
Fixpoints, POPL 1977, 1977, pp. 238–252.
[ 6 ] de Moura, L. M. and Bjørner, N.: Z3: An Efficient SMT Solver, Tools and Algorithms for theConstruction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Partof the Joint European Conferences on Theory andPractice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, 2008,
pp. 337–340.
[ 7 ] de Oliveira, S., Bensalem, S., and Prevosto,
V.: Polynomial Invariants by Linear Algebra, Automated Technology for Verification and Analysis 14th International Symposium, ATVA 2016, Chiba,
Japan, October 17-20, 2016, Proceedings, 2016,
pp. 479–494.
[ 8 ] Kennedy, A.: Dimension Types, Programming
Languages and Systems - ESOP’94, 5th European
Symposium on Programming, Edinburgh, U.K.,
April 11-13, 1994, Proceedings, 1994, pp. 348–362.
[ 9 ] Kojima, K., Kinoshita, M., and Suenaga, K.:
Generalized Homogeneous Polynomials for Eﬃcient Template-Based Nonlinear Invariant Synthesis, Static Analysis - 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10,
2016, Proceedings, 2016, pp. 278–299.
[10] Müller-Olm, M. and Seidl, H.: Computing
polynomial program invariants, Inf. Process. Lett.,Vol. 91, No. 5(2004), pp. 233–244.
[11] Padhi, S., Sharma, R., and Millstein, T. D.:
Data-driven precondition inference with learned features, Proceedings of the 37th ACM SIGPLAN
Conference on Programming Language Design and
Implementation, PLDI 2016, Santa Barbara, CA,
USA, June 13-17, 2016, 2016, pp. 42–56.
[12] Rodrı́guez-Carbonell, E. and Kapur, D.: Generating all polynomial invariants in simple loops, J.
Symb. Comput., Vol. 42, No. 4(2007), pp. 443–476.
[13] Sankaranarayanan, S., Sipma, H., and Manna,Z.: Non-linear loop invariant generation usingGröbner bases, POPL 2004, 2004, pp. 318–329.

[14] Sharma, R., Gupta, S., Hariharan, B., Aiken, A.,
Liang, P., and Nori, A. V.: A Data Driven Approachfor Algebraic Loop Invariants, Programming Languages and Systems - 22nd European Symposiumon Programming, ESOP 2013, Held as Part of theEuropean Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March
16-24, 2013. Proceedings, 2013, pp. 574–592.
[15] Winskel, G.: The Formal Semantics of Programming Languages: An Introduction, MIT Press,
Cambridge, MA, USA, 1993.

A 補題の証明(証明) (補題 4.1)
まず a ∈ A について A − a が線形空間になるとき，任意の b ∈ A について A − b が線形空間になることを示す，任意に a′ , b′ ∈ A − b を選ぶ．

• a′ + b′ ∈ A − b であること: a′ + b ∈ A かつ
b′ + b ∈ A なので a′ + b − a, b′ + b − a ∈ A − a．
b − a ∈ A − a であることと A − a が線形空間であることより，a′ + b′ + b − a = (a′ + b − a) + (b′ +b − a) − (b − a) ∈ A − a．よって，a′ + b′ ∈ A − b．
• 任意の k ∈ R について ka′ ∈ A − b である
こと: a′ + b − a, b − a ∈ A − a であることとA − a が線形空間であることより，ka′ + b − a =k(a′ + b − a) − (k − 1)(b − a) ∈ A − a．よって
ka′ ∈ A − b．
よって，A − b は線形空間である．
次に，任意の a, b ∈ A について，A − a = A − bとなることを示す．任意の a′ ∈ A − b について，

a′ + b − a ∈ A − a となり，b − a ∈ A − a であることと A − a が線形空間であることより，a′ ∈ A − a．
よって，A − b ⊆ A − a．同様にして A − a ⊆ A − bが示せるので，A − a = A − b．

(証明) (補題 4.2) A′u,v が空でないので T ′ ∈ A′u,v を取れる．定義より A′u,v − T ′ = {T − T ′ |u = T v ∧ T ∈A} であるが，u = T ′ v であるから ，この集合 は
A := {T −T ′ |(T −T ′ )v = 0∧T ∈ A} = v ⊥ ∩(A−T ′ )に等しい．よって A は線形空間であり，A′u,v は aﬃnesubspace である．
(証明) (補題 4.3) B ⊆ A のとき，b ∈ B について

B − b ⊆ A − b であるが，B − b と A − b は線形

る．S ⊆ T0′ は明らかである．S ⊆ Tk′ を仮定する．T ′空間なので，B − b は A − b の線形部分空間であを 10 行目で選ばれた Tk′ の元とし，σ を 14 行目で選ばる．よって dim(B − b) ≤ dim(A − b) であるかられた φ[σ/⃗x]∧ ̸|= {B = JBKσ }c{B = T ′ JBKσ } を満た

dim B ≤ dim A となる．dim A = dim B のときは，す状態，すなわち σ |= φ かつ ̸|= {B = JBKσ }c{B =dim(A − b) = dim(B − b) となるが，B − b は A − b

T ′ JBKσ } なる状態とする．アルゴリズムの定義かの線形部分空間だから A − b = B − b である．よって′ら ，Tk+1= Tk′ ∩ {T | JBKJcKσ = T JBKσ }．帰 納 法

A = B．

′の仮定 S ⊆ Tk′ より，S ⊆ Tk+1を示すためには，(証明) (補題 4.4)
T ′ ⊆ T であることは明らか．ここで，T = T ′ と仮 定 す る と ，任 意 の T ∈ T で JBKJcKσ = T JBKσと な る た め ，JBKJcKσ = T ′ JBKσ と な る ．よって ，{B = JBKJcKσ }c{B = T ′ JBKσ } と な る が ，こ れ は
σ の定義に矛盾する．以上より，T ̸= T ′ となるため，
T′ ⊊T．
(証明) (補題 4.5) n に関する数学的帰納法で証明すS ⊆ {T | JBKJcKσ = T JBKσ } を示せば十分である．任意に S ∈ S を選ぶ．S の定義より，∀⃗a.φ[⃗a/⃗x] =⇒|= {B = JBK⃗a }c{B = SJBK⃗a }．よって，σ |= φ な
らば，|= {B = JBKσ }c{B = SJBKσ }．仮定より実際に σ |= φ なので，|= {B = JBKσ }c{B = SJBKσ }．
よって |= {A}c{B} の定義と σ |= B = JBKσ が成り立つことから JcKσ |= B = SJBKσ ．したがって，

JBKJcKσ = SJBKσ ．