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

帰納的述語定義を含む分離論理における循環証明による半自動証明
仲田 壮佑

中澤 巧爾

帰納的述語定義を含む分離論理によるプログラムの自動検証に向けて，論理式の半自動証明器を実装した．より具体的には，Brotherston らの提案した循環証明体系における証明探索を行なう．循環証明体系による証明では，特定の条件のもとで証明木に循環を許し，帰納的に定義された述語を含む論理式の証明を行う．証明探索の際には帰納的述語を定義に従って展開する必要があるが，素朴な方法では適用可能な推論規則の数が爆発的に増加する．展開する述語の選び方と適用する推論規則の順番を制限し，探索の枝刈りを行った．以上のアイディアに基づき，証明探索を行う
自動証明器を実装した．本研究で実装した証明器を用いて，様々な帰納的述語定義を含む論理式の自動証明を行った．また，証明可能なときには，証明器に証明木を出力させ，証明探索によって発見された証明を可視化した．

We implement a semi-automated prover for implicational formulas (entailments) of the separation logic including inductive
predicate definitions, toward automation of program verification by separation logic. More specifically, we use cyclic proof
system, proposed by Brotherston et al., to construct proof. In cyclic proof system, we allow proof trees to contain cycles
under a specific condition and prove entailments including inductive predicates. We must unfold inductive predicates inaccordance with their definition. In a naı̈ve way, the number of applicable inference rules increases explosively. For pruning,
we restricted the selection method of predicates to be unfolded and the order of applications of the inference rules. Basedon the above idea, we implemented an automated prover searching for a proof. We automatically proved several entailmentswith inductive predicates by using the prover implemented in this paper. Besides we let the prover output proof trees as LATEX
code if the entailment is provable, and we visualized the proofs found by proof search.

を実行し，停止すれば，必ず事後条件 ψ を満たすこ

1 はじめにとを {ϕ}C{ψ} と表し，これをホーアの三つ組と呼ぶ．

プログラムの正当性を実行前に保証する手法の一

とくに分離論理では，条件 ϕ，ψ によってヒープの状つとして分離論理 [6] がある．分離論理はホーア論理

態を表現できる．論理体系においてホーアの三つ組ををポインタを操作するコマンドとヒープ状態を表す

証明する際，多くの場面で条件式の含意 ϕ1 |= ϕ2 の正条件によって拡張したものである．現実のプログラム

しさを判定する必要がある．ここで，ϕ1 |= ϕ2 は，条は，ヒープ領域のメモリ操作を含むものが多く，その件 ϕ1 を満たす任意のヒープが条件 ϕ2 を満たすこと

ようなプログラムの正当性検証に即した分離論理は，を表す式で，判断式（entailment）と呼ばれる．

近年盛んに研究されている．

本研究では，帰納的に定義された述語を含む分離

ホーア論理およびその拡張の分離論理ではホーアの論理において ϕ1 |= ϕ2 の形の判断式の妥当性を自動判

三つ組（Hoare triple）を用いてプログラムの性質を表定することを目標とし，Brotherston による循環証明

現する．事前条件 ϕ が成立するときにプログラム C

体系 [2] [3] における半自動証明手続を提案する．さらSemi-automated Entailment Checker by Cyclic Proofs for
Separation Logic with Inductive Predicates.
Sosuke Nakada and Koji Nakazawa, 名古屋大学大学院情報科学研究科情報システム学専攻, Dept. of Information Engineering, Graduate School of Information Science, Nagoya
University.

に，その実装を与え，いくつかの実行例を示す．
帰納的に定義された述語に関する性質は帰納法によって証明されることが多い．帰納法では，証明しようとしている主張を帰納法の仮定として利用するが，これを循環する証明木の形で実現したものが循環証

明体系である．循環証明体系では帰納法の仮定に当

ここで，P は帰納的述語であり，各帰納的述語のアリたる部分を結論と繋ぐことでできる循環構造を証明

ティは固定とする．表記の便宜上，分離論理における木に含むことを許す．しかし，循環証明体系において

結合（∗）は論理積（∧）より記号としての結合が強は，述語を帰納的定義によって展開することによっていものとする．

証明探索を進めるため，どの述語をどのタイミングで展開するか，を考えなければならず，素朴な方法では考慮すべき場合の数が爆発することがある．

述語 P の帰納的定義とは，n∨P(⃗t) =∃⃗zi .ϕi （⃗zi = FV(ϕi ) − ⃗t）i=0の形の式とする．各 ∃⃗z.ϕi を P の定義節と呼ぶ．述語

一般に，帰納的述語を含む判断式に対する循環証明の帰納的定義の有限集合 I が帰納的定義集合であるを構成するためには，判断式の左辺と右辺において対とは，I が各 P に対する帰納的定義を高々一つしか含応するメモリ領域について言及している述語を発見

まず，定義節中に出現する任意の述語 Q について，Iし，それらを帰納的定義に沿って展開することで循環が Q の帰納的定義を含んでいることをいう．以下で構造を発見できることが多い．これは，場合分けと帰は，一つの帰納的定義集合を固定して考えているもの

納法の仮定を用いた通常の帰納法による証明に相当すとする．

る．本研究では，この判断式の両辺において対応する

次に分離論理の意味論を与える．変数は，値として述語を探すために，推論規則の適用の順序を制御し，メモリ上のロケーションまたは nil をとるが，ここでまた，帰納的定義の展開を制限する．これにより，効はロケーションを 0 以外の自然数，nil を 0 として解率的な証明探索が実現できると考えられる．

釈する．

さらに，本研究で提案する手続を実装した証明器

Val

:=

N

によって，いくつかの判断式の例の妥当性を判定し，

Locs

:=

N\{0}

これらの判断式に対して確かに証明を与えられるこ

メモリ状態を表すのは組 (s, h) である． s はストアととを確認した．さらに，証明可能な判断式に対しては呼ばれ，変数に対する値（Val）の割当てを表現する．

その証明を証明図の形で出力するようにし，証明の可また h はヒープと呼ばれ，各ロケーションへの値（の視化を行なった．

組）の割当てを表現する．値が割当てられているメモ

本論文の構成は以下の通りである．第 2 節では分離論理及び帰納的述語定義を与える．第 3 節では循環

リ領域は有限であるとする．すなわち，ストアとヒー
プは次のような集合の要素である．

証明体系を定義する．第 4 節では本研究が提案するStores:=証明探索の手続について解説し，第 5 節では第 4 節

Heaps

:=

のアイディアにもとづいて実装した証明器による実行
例を載せる．最後に第 6 節で本研究のまとめと今後の課題を述べる．

Vars → Val∪
Locs → f in
Valn
n≥1

任意のストアは， s(nil) = 0 によって，項から Valへの関数だと思える．h の定義域を Dom(h) で表す．
二つのヒープ h1 と h2 について，h = h1 + h2 とは，Dom(h1 ) ∩ Dom(h2 ) = ∅ かつ h が次のようなヒープで2 分離論理あることを意味する．

分離論理の項（t, t1 , t2 ,. . . ）は，変数（ x, y, z,. . . ）または定数 nil である．変数全体の集合を Vars と書
く．本論文で扱う論理式は，シンボリック・ヒープ（symbolic heap）と呼ばれるもので，以下のとおり定義される．
ストア論理式 Π::=t =t |t ,t |Π∧Π

ヒープ論理式 Σ::=

emp | t 7→ (⃗t) | Σ ∗ Σ | P(⃗t)

論理式 ϕ

::=

Π∧Σ

n ∈ Dom(h1 ) のとき h(n)=h1 (n)n ∈ Dom(h2 ) のとき h(n)=h2 (n)

メモリ状態 (s, h) が ϕ を満たすことを s, h |= ϕ と表し，以下で定義する．

s, h |= t1 = t2

iﬀs(t1 ) = s(t2 )s, h |= t1 , t2

iﬀs(t1 ) , s(t2 )s, h |= Π1 ∧ Π2iﬀ

s, h |= Π1 かつ s, h |= Π2

s, h |= emp

iﬀ

Dom(h) = ∅s, h |= t 7→ (⃗t)

iﬀ

Dom(h) = {s(t)} かつ h(s(t)) = s(⃗t)

s, h |= Σ1 ∗ Σ2iﬀ

∃h1 , h2 (h = h1 + h2 かつは fresh であるとする．また，(UnfLP)，(UnfRPi ) におn∨いて，P は P(⃗t) =∃⃗zi .ϕi で定義されているとする．

s, h1 |= Σ1 かつ s, h2 |= Σ2 )(Id)，(P Id)，(empL)，(empR) は [2] での (Id)，(∗)，

s, h |= P(⃗t)

iﬀs, h |= P0 (⃗t)
s, h |= Pk+1 (⃗t)

s, h |= Π ∧ Σ

iﬀ

iﬀ

ただし， (UnfLP) において θ = [⃗z := ⃗y] であり， ⃗yi=1∃n(s, h |= Pn (⃗t))(empL)，(empR) から導くことができる．(Id) は公理

は成立しないである．

P の定義節 ∃⃗z.ϕi と(UnfLP)，(UnfRPi ) を展開規則と呼び，これらの規値の列 ⃗n が存在して則を適用することを述語を展開すると呼ぶ．述語を展s[⃗z := ⃗n], h |= ϕi [P := Pk ](⃗t)

開することで，証明木の祖先と変数名以外が同じ判断

s, h |= Π かつ s, h |= Σ式が現れることがある．次の例で示す．

判断式 ϕ1 |= ϕ2 は「任意の (s, h) に対して， s, h |= ϕ1

ls(x, y)ならば s, h |= ϕ2 」と定義する．

=∨

3 循環証明体系

x = y ∧ emp
′

′

(ϕ1 )
′

∃x .x 7→ x ∗ ls(x , y)(ϕ2 )

図 1 において，結論の ls(x, x′ ) ∗ ls(x′ , y) ⊢ ls(x, y) は

本論文では，与えられた ϕ1 , ϕ2 における ϕ1 |= ϕ2 の波線部と名前替えをして等しい関係にある．この時，妥当性を判定することを目標として， ϕ1 ⊢ ϕ2 の証明

述語が帰納的に定義されていることから，ある条件下探索を行い，自動証明を行う証明器を実装する．本節でこれを公理と同じように扱い，証明に循環を許すこ

では，証明探索のための推論規則と循環証明の定義をとができる．これを循環証明という．循環証明を適用行う．

できる条件を述べる前に，トレース（trace）について

以下の推論規則を用いる．

述べる．

Π1 ∧ emp ∗ Σ1 ⊢ Π2 ∧ Σ2
(empL)
Π1 ∧ Σ1 ⊢ Π2 ∧ Σ2
Π1 ∧ Σ1 ⊢ Π2 ∧ emp ∗ Σ2
(empR)
Π1 ∧ Σ1 ⊢ Π2 ∧ Σ2
(Π1 ∧ Σ1 ⊢ Π2 ∧ Σ2 )[t2 := t1 ](=L)
t1 = t2 ∧ Π1 ∧ Σ1 ⊢ Π2 ∧ Σ2
Π1 ∧ Σ1 ⊢ Π2 ∧ Σ2 t1 , t2 ∧ Π1 ∧ Σ1 is UNS AT(=R)Π1 ∧ Σ1 ⊢ t1 = t2 ∧ Π2 ∧ Σ2

証明木において対応する述語の列を考える．図 1 では，ls(x, x′ ) に着目すると，右の枝では述語が展開さ
れて ls(z, x′ ) になる．次の推論規則適用では変わらずに ls(z, x′ ) である．このような述語の列を ls(x, x′ ) のトレースと呼ぶ．厳密な定義は [2] による．
循環証明は以下を満たすときに認められる．
判断式 Γ1 ⊢ Γ′1 に対する推論規則の適用によって判断式 Γ2 ⊢ Γ′2 となったとき，• ∃θ.(Γ1 ⊢ Γ′1 )θ = Γ2 ⊢ Γ′2

Π1 ∧ Σ1 ⊢ Π2 ∧ Σ2 t1 = t2 ∧ Π1 ∧ Σ1 is UNS AT(=/R)Π1 ∧ Σ1 ⊢ t1 , t2 ∧ Π2 ∧ Σ2

• Γ1 , Γ2 内の同じ位置での P の出現で，それぞれΠ ∧ Σ1 ⊢ Σ2
(P Id)Π ∧ Σ ∗ Σ1 ⊢ Σ ∗ Σ2

ス内で (UnfLP) が適用されているようなものがΠ1 ∧ emp ⊢ emp(Id)の P は同じトレースに属しており，そのトレー存在する．
葉が公理であるか，循環証明の条件を満たす証明木Π ∧ϕ1 θ ∗ Σ1 [⃗t := ⃗xθ] ⊢ Σ2 [⃗t := ⃗xθ]…
Π ∧ϕn θ ∗ Σ1 [⃗t := ⃗xθ] ⊢ Σ2 [⃗t := ⃗xθ]Π ∧ P(⃗t) ∗ Σ1 ⊢ Σ2が構築できる場合，これを証明とする．
図 1 では結論中の ls(x, x′ ) と 波線部中の ls(z, x′ ) が(UnfLP)Π ∧ Σ1 ⊢ ϕi [⃗z := ⃗y] ∗ Σ2
(UnfRPi )Π ∧ Σ1 ⊢ P(⃗t) ∗ Σ2

同じトレース内にあり，トレース内の述語に (UnfLls)が適用されているので，ls(x, x′ ) ∗ ls(x′ , y) ⊢ ls(x, y) の証明となっている．

emp ⊢ emp (Id)ls(z, x′ ) ∗ ls(x′ , y) ⊢ ls(z, y)(P Id)::::::::::::::::::
emp ∗ ls(x, y) ⊢ emp ∗ ls(x, y)(empR)(P Id)
emp ∗ ls(x, y) ⊢ ls(x, y)
x 7→ z ∗ ls(z, x′ ) ∗ ls(x′ , y) ⊢ x 7→ z ∗ ls(x, y)(=L)(UnfRls2)x = x′ ∧ emp ∗ ls(x′ , y) ⊢ ls(x, y)
x 7→ z ∗ ls(z, x′ ) ∗ ls(x′ , y) ⊢ ls(x, y)(UnfLls)ls(x, x′ ) ∗ ls(x′ , y) ⊢ ls(x, y)
図1

この条件は [2] の global trace condition の十分条件

4. 2 拡張判断式となっている．従って，我々の証明体系は [2] の部分

2 節で定義した判断式を拡張する．入力 J が与えら体系となっている．循環証明の健全性は [2] で示されたときに，J に含まれる帰納的述語それぞれを区別れている．すなわち，ϕ1 ⊢ ϕ2 が循環証明を持てば，する番号を付ける．これをタグと呼ぶ．帰納的述語 P

ϕ1 |= ϕ2 である．

のタグが i である場合，Pi と表記する．次に，証明木において祖先となるノードの判断式の列である α と証

4 実装の考え方

明木において左辺の展開規則 (UnfLP) がいくつ前に

本節では実装において必要な判断式の拡張と証明適用されたかを示す π を定義する．α は空列， π は 0を高速に行うための推論規則の適用順序について述が初期値であり，推論規則を適用する毎にそのときのべる．

判断式を α に加え，π を 1 増やす．ただし，(UnfLP)

以下で，証明探索のための手続きを与える．以後，判断式 J と帰納的定義集合 I を入力とし，出力は「妥当である」「妥当でない」「不明」の 3 通りであるとする．
なお，実装ではヒープ論理式をリストで表し， empの場合は π を 0 にする．
循環証明に相当する規則 (Downlink) を以下で定義する．

|α| > n > π∃θ.αn = (ϕ1 ⊢ ϕ3 )[θ] ϕ2 matches ϕ3(Downlink)(α, π, ϕ1 ⊢ ϕ2 )は空リストとして扱う．よって，(empL) 及び (empR)

matches はタグを無視して等しいことを表す．これは，については以後は考えない．

[2] の拡張判断式（augmented sequents）による．
次に，J の左辺及び右辺のタグ付き述語を 1 つずつ

4. 1 正規化

要素に持ったそれぞれの列 qL , qR と，次の展開規則を

任意の判断式 Π1 ∧ Σ1 ⊢ Π2 ∧ Σ2 は，3 節で述べた

左辺と右辺どちらを優先するべきかを表す真偽値 fL

正規化をすることで Π′1 ∧ Σ′1 ⊢ Σ′2 の形に変形可能であを定義する．これらによって述語の展開順序を制御する．ただし，Π′1 は t1 = t2 の節を含まない．本論文でる．qL , qR の初期値はそれぞれ左辺，右辺のタグ付きは，これを正規形の判断式であると呼ぶ．

述語を 1 つずつ要素に持っているが，順序は任意に定(=R)，(=/ R) では充足可能性判定をし，論理式が充めてよい． fL の初期値は真である．

足可能でない場合にのみ規則を適用できるが，充足可fL が真の場合は qL , qR の順に，偽の場合は qR , qL

能であるとした場合には即座に「妥当でない」を出力の順に繋いだ新たな列 q を作る．q の先頭の述語をする．Π1 ∧ Σ1 ⊢ Π が妥当でなければ，その充分条件(UnfLP) または (UnfRPi ) によって展開する．(UnfRPi )の Π1 ∧ Σ1 ⊢ Π ∧ Π2 ∧ Σ2 も妥当でないからである．

は全ての i について試みる．その後証明ができなかっ正規化は正規形でない判断式が現れた場合に即座た場合は q の 2 番目の述語を同様に列の最後まで続けに行われる．(=L)，(=R)，(=/ R) をそれ以上適用不可

る．展開のとき，展開する述語のタグが qL に含まれて能であるまで適用する．

いれば，それを 削除し，展開した後に現れる述語を qLの末尾に加える．展開する述語のタグが qR に含まれていれば，それを削除し，展開した後に現れる述語を

qR の末尾に加える．また，(UnfLP) を適用した場合はfL を偽に，(UnfRPi ) を適用した場合は fL を真にする．
例えば，qL = [P1 ; P2 ; Q3 ], qR = [P4 ; Q5 ] のときに P2が展開された場合は，qL = [P1 ; Q3 ; P2 ], qR = [P4 ; Q5 ]明を生成できるような変数の取り方をすべきである．
ここで， P の帰納的定義の定義節が以下の形で記述してあるとする．

∃⃗z.ϕi = ∃⃗z.x 7→ (⃗y) ∗ ϕ′i
左辺になんらかの項列 ⃗v による x 7→ (⃗v) が含まれてとなり， fL は偽となる．
展開規則を適用する順や条件を細かく指定する理いる場合に，⃗y を ⃗v にマッチングする．ただし，マッ由を述べる．循環証明では，両辺の対応する述語を展

チングの変数は ⃗z とする．マッチングが可能であった開することが必要である．そのため左辺と右辺を交場合， x 7→ (⃗y) ∗ ϕ′i に対してマッチング結果である ⃗z

互に展開することをまず試みる．ただし，左辺と右辺への代入を行い，(UnfRPi ) を適用する．マッチング

それぞれどの述語が循環証明に対応する述語か分かができない場合は展開を行わない．

らないため，それを順繰りに試すために qL , qR を用い

これは，左辺に x 7→ (⃗v) が含まれていない場合，新る．本論文の実装では，可能な展開順全てを試していたに右辺に現れる x 7→ (⃗y) によって証明ができなくな

ることになる．

るためである．左辺に x 7→ (⃗y) を含む判断式を公理か

しかし，左辺や右辺を連続で展開しなくてはならな

左辺にも x 7→ (⃗y) が含まれているべきである．そのたい場合も存在する．例えば，3 節の ls と，

ls2(x, y)=|x = y ∧ emp′′′

ら導くには (P Id) 規則を用いざるを得ない．よって，
め左辺に x 7→ (⃗v) が含まれている場合のみ (UnfRPi )

′

′

′′

′′

∃x , x .x 7→ x ∗ x 7→ x ∗ ls(x , y)規則を適用する．

で定義される ls2 による ls2(x, y) ⊢ ls(x, y) は右辺を連続で展開する必要がある．そのため qL , qR を結合し，4. 4 適用順序

左辺や右辺を連続で展開する場合をも計算している．

証明器は J から拡張判断式を作り，拡張判断式を

これは左辺や右辺を交互に展開することを試みた後推論規則に相当する操作によって変形していく．初期に試みられる．

値は α = [], π = 0, qL = [], qR = [], fL = 真, c = 0 であ

また，実行時には (UnfLP) を無限に適用可能である．ただし，[] は空列である．

るので，証明器が有限で止まらなくなる可能性があ「 正 規 化 」 ，「(Id)」,「(P Id)」,「(Downlink)」,

る．展開回数の上限 dmax を与えて，証明器を有限で「(UnfLP) または (UnfRPi ) の適用の操作」をこの順止まるようにする．ただし，展開回数の上限を超えて序で適用し，新たに拡張判断式が得られた場合はそ展開できずに証明ができなかった場合は結果を「不の拡張判断式に対して繰り返してこれを適用する．

明」として出力する．そのために現在の展開回数を記「(UnfLP) または (UnfRPi ) の適用の操作」において憶する d を新たに定義する．

c > cmax あるいは (UnfRPi ) が条件に合わずに展開さ本論文では J, α, π, qL , qR , fL , d を合わせて拡張判断式と呼ぶ．

れない場合は「不明」を出力する．正規化できなかったとき，または述語が一つもなくどのどの推論規則も適用できない場合は「妥当でない」を出力する．全て

4. 3 (UnfRPi ) の適用の制限の葉で (Id) または (Downlink) が適用可能で，証明木(UnfLP) 規則によって帰納的述語を展開することでが構築できた場合「妥当である」を出力する．

新しく現れる変数は判断式で既に使われているもの
以外でなければならない．一方，(UnfRPi ) 規則によっ

5 実行例て帰納的述語を展開することで新しく得られる変数

5. 1 実行内容

は制約はない．

4 節に従って自動証明器のプログラムを OCaml で記

実装においては， (UnfLP) 規則ではとにかく新たな述し，表 1 で定義される述語を含む表 2 の判断式を入変数を導入すればよいが，(UnfRPi ) 規則では循環証

力として証明器を動作させた．dmax は 4 および 10 で実行した．構文解析部及び，シンボリックヒープの充先に発見されたためと考えられる．幅優先探索をする

足可能性判定器は東邦大の木村による実装を利用した．

プログラムに変更することで改善されると思われる．

この充足可能性判定は [4] のアルゴリズムの基づくもの

図 3 において，番号 1,5 は実行時間が dmax = 4 とである．動作環境は DELL optiplex 9020, プロセッサはdmax = 10 でほぼ変わらなかった．番号 2,3,4 は同じタIntel(R) Core(TM) i7-4790 CPU @ 3.60GHz 3.60GHz，グの述語を連続で展開する必要があるが，番号 1,5 は

メモリは 8GB，1600MHz DDR SDRAM デュアルイ

交互に展開をするだけなので，dmax によらず即座に証

ンターリーブ， OS は Windows 10 Pro で仮想マシ

明を発見できたためであると考えられる．

ン VMware(R) Workstation 12 Player バージョン 12.1.0

build-3272444 を使って Ubuntu 15.04 64 ビットを起

6 おわりに動し，RAM 2GB, プロセッサ数 2 の設定で，OCaml

6. 1 まとめversion 4.01.0 にて動作させた．実行を 5 回行い，そ本研究では帰納的述語を含む分離論理によるプロれぞれの実行時間の平均値の 1/10 ミリ秒の位を四捨グラム検証の自動化に向けて，含意を表す判断式の五入して実行時間とした．

半自動証明手続を提案し，その実装を与えた．実装でまた，証明可能だった場合は証明木を LATEX ファイ
ルに出力させて可視化した．

はプログラムが有限で止まるように展開の回数の上限を定めた．述語展開の順序を制御することにより，効率のよい証明探索を目指した．また，証明可能な場

5. 2 結果
表 2 の判断式を入力として証明器を動作させたときの実行時間を表 3 に示す．

合は証明図を出力するようにした．
例として様々なリストを含む判断式を入力として動作させ，正しい結果が得られることを確認した．その

d = 4 では表 2 の全ての例で証明ができた．d = 10

際，展開の回数の上限を大きくすると実行時間が増

では全ての例で証明ができたが，全て実行時間がほぼえ，一部の例では出力させた証明木の形が異なった．

同じか増え，また証明木の形が d = 4 とは異なるもの

展開の回数が増えたために循環証明に関係のない述もあった．

語の展開をも行ったものが先に証明として発見された

表 2 の番号 1,4 の証明木を図 2,3 に示す．そのほかためと思われる．

の証明木については付録 A に載せる．

6. 2 関連研究と今後の課題
5. 3 考察

制限のないシンボリック・ヒープに対する妥当性判

証明木の形が異なったのは循環証明に関与しない述定は決定不可能であることが知られている [1]．従っ

語の展開を含んでいたためであった．図 4 は表 2 の番て，妥当性判定を完全に決定するためには論理式に

号 4 の d = 10 での証明木であり，図 3 と形が異なっ

一定の制限を課すことが必要である．判断式の妥当ている．

性判定についての既存研究としては， [2] [3] [5] など

dmax = 10 では実行時間が増えているが，dmax が大がある． [2] [3] は本研究と同様に循環証明を用いた

きいほど適用可能な規則のパターンが多いためであ

証明探索であり， [5] はオートマトンによる手法である． [2] の推論規則 (∗) をそのまま用いる場合，dmax

る． [2] [3] では妥当性判定は高速であるが述語定義にが大きくなったときに推論規則の適用パターンが爆発

制約が設けられている．対して， [5] はより一般の述的に多くなるが，本論文の定義ではその場合より時間

語定義において決定可能であるがより時間がかかる．

の増加を抑えられているといえる．

本研究の証明器は多くの判断式について [2] より速く，

証明木の形が異なったのは深さ優先で探索をしたた[3] と同等程度の速度で証明をした．本研究で提案しめ，dmax = 4 では打ち切られて発見されなかった，循

た手続きによって妥当性が決定できる判断式のクラス

環証明に関与しない述語の展開を含んでいる証明がを明らかにすること，また，より高速な証明探索を実

表1

述語

意味

ls

空リストを含むリスト

lsE/lsO

述語の定義

定義

ls(x, y)空リストを含む，長さがlsE(x, y)（偶数／奇数）のリスト

lsO(x, y)DLL

空リストを含まない双方向リスト

表2

番号

1

DLL(a, b, c, d)=

x = y ∧ emp∨∃x′ .x 7→ x′ ∗ ls(x′ , y)=x = y ∧ emp∨∃x′ .x 7→ x′ ∗ lsO(x′ , y)=∃x′ .x 7→ x′ ∗ lsE(x′ , y)=a = b ∧ c = d ∧ emp∨∃x.a 7→ (x, d) ∗ DLL(x, b, c, a)

証明した判断式

意味

判断式

ls(x, y) ∗ ls(y, z) ⊢ ls(x, z)

リストの結合奇数の長さのリストと

2

lsO(x, y) ∗ lsO(y, z) ⊢ lsE(x, z)

奇数の長さのリストの結合が偶数の長さのリストになること
奇数の長さのリストと

3

lsO(x, y) ∗ lsE(y, z) ⊢ lsO(x, z)

偶数の長さのリストの結合が奇数の長さのリストになること
偶数の長さのリストと

4

lsE(x, y) ∗ lsE(y, z) ⊢ lsE(x, z)

偶数の長さのリストの結合が偶数の長さのリストになること

5

DLL(x5 , x2 , x3 , x6 ) ∗ DLL(x1 , x5 , x6 , x4 ) ⊢ DLL(x1 , x2 , x3 , x4 )双方向リストの結合
表3

番号

判断式の証明時間．d は展開回数の上限．

d = 4 での実行時間（ミリ秒） d = 10 での実行時間（ミリ秒）

1

3

4

2

4

7

3

0

22

4

6

43

5

22

21

現するし，既存の証明器との性能比較を行うことは今

ことは興味深い問題である．

後の課題である．
また，本研究で考えている循環証明体系の完全性について考察することも今後の課題である．予想として，この体系は完全ではない，すなわち，妥当な判断式であって，証明不可能なものが存在する．一定の判断式のクラスに対して完全な循環証明体系を与える

参考文献[1] Antonopoulos, T., Gorogiannis, N., Haase, C., Kanovich,M., and Ouaknine, J.: Foundations for decision problems inseparation logic with general inductive predicates, International Conference on Foundations of Software Science andComputation Structures, Springer Berlin Heidelberg, 2014,
pp. 411–425.

図2

表 3 の番号 1 の d = 4 での証明木

図3

表 3 の番号 4 の d = 4 での証明木

図4

表 3 の番号 4 の d = 10 での証明木[2] Brotherston, J., Distefano, D. and Petersen, R. L.: Automated cyclic entailment proofs in separation logic, Automated Deduction (CADE-23), Springer, 2011, pp. 131-146.
[3] Brotherston, J., Gorogiannis, N. and Petersen, R. L.: A
generic cyclic theorem prover, Programming Languages
and Systems, Springer, 2012, pp. 350-367.
[4] Brotherston, J., Fuhs, C., Pérez, J. A. N., and Gorogiannis, N.: A decision procedure for satisfiability in separation logic with inductive predicates, Proceedings of the Joint
Meeting of the Twenty-Third EACSL Annual Conference on
Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science(LICS), ACM, 2014, p. 25.
[5] Iosif, R., Rogalewicz, A. and Vojnar, T.: Deciding entail-ments in inductive separation logic with tree automata, Automated Technology for Verification and Analysis, Springer,
2014, pp. 201-218.
[6] Reynolds, J. C.: Separation logic: A logic for shared mutable data structures, Logic in Computer Science, 2002. Proceedings. 17th Annual IEEE Symposium on, IEEE, 2002,
pp. 55-74.

A 付録: 5 節の実行結果
5 節で使用した証明器によって LATEX ファイルで出力された証明木をコンパイルして得られた証明木を載せる．5 章で載せたものについては省く．

図5

表 3 の番号 1 の d = 10 での証明木

図6

表 3 の番号 2 の d = 4 での証明木

図7

表 3 の番号 2 の d = 10 での証明木

図8

表 3 の番号 3 の d = 4 での証明木

図9

表 3 の番号 3 の d = 10 での証明木

図 10

表 3 の番号 5 の d = 4 での証明木

図 11

表 3 の番号 5 の d = 10 での証明木