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

プログラム操作のためのホーア論理の拡張
森口 草介

本論文では、ソースコードをユーザ定義のデータ型によって表現し、編集をそのデータ型に対する操作として捉えることで、ソースコードを編集するプログラムに対する、ホーア論理を用いた検証手法を提案する。ソースコードを編集するプログラムは、コード生成からコンパイラまで広く存在する。編集対象のソースコードは、操作するプログラムからはただのデータに過ぎず、プログラムの誤りにより意図しない形に編集してしまう。提案手法では、編集する対象に関するホーアの三つ組を記述できるようにすることで、編集の前後におけるソースコードを検証し、それを通じて編集するプログラムの検証を行う。編集対象のホーアの三つ組は、意味上は他の表明と同様に扱われるため、これ自体には論理体系の大きな変更を必要としない。しかし、三つ組自体が成立するかは少なくとも通常の検証と同程度に難しく、これを検証するための手法が必要である。編集対象であるソースコードは操作する側のパラメータとして表現されるため、検証時にパラメータで表された複数のプログラム間の関係を議論しなければならない。このために、ホーア論理の拡張として、三つ組同士の関係を取り扱う体系を考える。

In this paper, we propose an extension of Hoare logic for source code manipulations. There are so many programs whose
domain is a source code, e.g., code generators, compilers, and so on. In these programs, the target codes are denoted asdata. Our method is a framework for viewing such data as other programs and describing the specifications of the data as
behaviors of corresponging programs. These data are modified in execution, so our method introduces the rules for the datawith variables of the programs.

る結果を出す、といったものも多く報告されている。

1 はじめに最適化などのプログラム操作における仕様は、操作前ソースコードを編集するプログラムは、コード生成後の（または出力した）プログラムの挙動に関するも器やコンパイラなど広く存在する。コード生成では与のである。そのため、プログラム操作に関して検証をえられたデータに基づくプログラムの生成や、部分的行うには、対象プログラムの挙動を記述できる必要がなテンプレートの生成などがある。また、コンパイラある。

やプログラム解析では入力としてソースコードを用

本論文では、対象プログラムをユーザ定義のデータい、別のデータを出力とする。以下、このように別の型によって表現し、プログラム操作をそのデータ型にソースコードを生成、解析、編集することをプログラ対する操作として記述したプログラムに対する、ホーム操作と呼び、操作されるプログラムを対象プログラ

ア論理を用いた検証手法を提案する。提案手法では、

ムと呼ぶ。

対象プログラムに関するホーアの三つ組を直接記述

対象プログラムは、操作するプログラムからはただできるようにすることで、仕様の記述を可能にする。のデータに過ぎず、誤りにより意図しない形に編集さしかし、記述されたホーアの三つ組は、プログラムをれる可能性がある。例えば、コンパイラでのバグとし対象としている以上、少なくとも通常のホーアの三つて、特定のソースコードに対して最適化前後で異な組と同程度に示すことが難しい。さらに、対象プログラムは操作するプログラムの変数として格納されてExtension of Hoare Logic for Program Manipulations
Sosuke Moriguchi, 関 西 学 院 大 学, Kwansei Gakuin
University.

いる場合もあり、その結果を基に編集したプログラムとの関係を推論する必要もある。そこで、推論規則を拡張し、対象プログラムに関する三つ組を検証できるようにする。この規則では、意味論による結果と推論規則を組み合わせることで、既存の手法を利用して検証を行う。
本論文の構成は以下の通りである。2 節では、プログラムを記述する言語として単純な手続き型言語である While 言語にデータ型の概念を追加したものについて述べる。3 節では、仕様を記述するための表明言語に関して述べる。4 節では、基礎となる推論規則

p := assign_s ("x",add(var("x"),int (10)));
if n <= 0 then s := skip_s ()else s := assign_s ("x", int (10));n := n - 1end;
while 0 < n dos := seq_s(s, p);n := n - 1endに関して述べる。5 節では、6 節では関連研究について述べ、最後に 7 節でまとめる。

例 え ば 、nの 初 期 値 が 3 の と き 、sに は seq_s(seq_s(p, p), assign_s("x", int(10)))（ただし2 対象言語

p=assign_s("x", add(var("x"), int(10))）が格

本論文では、簡易な手続き型言語である While 言納され、−1 のとき、sには skip_s()が格納される。

語を用いる。ここでは、データ構造を作るためコンス

また、次のプログラムは、いくつかのコンストラクトラクタを持つものとする。また、このコンストラクタで作られたデータに対して、パターンマッチを用いタを展開するために文構造としてパターンマッチを導ることで内部の情報を解析する例である。概要として入する。構文は図 1 の通りである。
パターンマッチの文構造は、関数型言語に見られるパターンマッチに対して以下の制約を置いたものとなっている。

1. パターンマッチの対象が式ではなく単一の変数である。 この制約は直前に代入を行うことで容易に回避できる。

2. コンストラクタに関する宣言がないため、パターンの網羅性などが判定できない。 今回は宣言やコンストラクタとパターンのパラメータ数、網羅性などについては議論せず、適切に記述されているものとする。

3. 一つのパターンマッチにおいてそれぞれのパターンにおけるコンストラクタは相異なるものとする。

4. パターンマッチの対象および各パターン内の変数は全て相異なる変数とする。
意味論は図 2 のようになる。対象言語である While
言語には局所変数の概念を入れていないため、パターンマッチでは単純な代入が行われている。
次のプログラムは、nの初期値に応じてコンストラクタをネストして構造を作っている。

は「assign_sの第一引数に nameに格納された値と同じものが格納されているようなものの数」を数えるものである。

count := 0;
rest := skip_s ();flag := 1;
while flag = 1 domatch prog with| skip_s () =>prog := rest;
rest := skip_s ()| assign_s (v, a) =>if v = namethen count := count + 1
else skip end;
prog := skip_s ()| seq_s(s1 , s2) =>prog := s1;
rest := seq_s(s2 , rest)end;
if prog = skip_s ()and rest = skip_s ()then flag = 0
else skip endend

v::=n|"string"|x||c(v1 , v2 , . . .)

E+E|

E::=v

b::=

true |

false

B::=b||

E<>E

S::=skip |x:=E||
図1

E=E|

E-E|

S ;S

E<=E|

E*E|

|

E<E

c(E1 , E2 , . . .)|B and B |if B then S else S end

B or B |notB| while B do S end

match x with | c(x1 , x2 , . . .) => S | . . . end
While 言語の構文。v が値、E が式、b がブール定数、 B がブール式、S が文。

なお、再帰的な構造の走査を単純な繰り返しにするため、restに対象プログラムの残りを格納している。

以下のように定義する。
F (skip_s())=skip

F (assign_s(”str”, a))=str := A(a)が 0 以上のとき、その値に 10 をかけたものを変数

F (seq_s(s1 , s2 ))=F (s1 ); F (s2 )xに格納するプログラムの生成」「progが表すプログ

F (if_s(b, s1 , s2 ))=if B(b) then F (s1 )ラムにおいて、nameに入った名前の変数へ代入する

else F (s2 ) end
この中では B や A を利用している。それぞれブー次節にて述べるが、これらはそれぞれ「nの初期値文の数え上げ」に相当する。ただし、コードが長くなるため、後者における対象プログラムは代入文と skip文を並べただけのものとなっている。

3 表明言語
表明言語は図 3 の通りである。ここで、 f はユーザ定義の、値から表明への全域関数である。なお、本論文では、 f を値の構造に関する再帰関数の形で定義する。
表明言語の定義において特徴的なのは以下の点である。

1. 表明言語中の変数にラベルが付与されている。
表明中に文構造があり、文構造内の変数と外側の変数を区別するために用いられる。

2. 文を生成する関数 F が存在する。
以降、While 言語の変数（ラベルが付与されていない）と区別するために、表明言語の変数（ラベルが付与されている）をラベル付き変数と呼ぶ。通常はWhile 言語の変数を単に変数と呼ぶが、差を強調する場合には、While 言語の変数をラベル無し変数と呼ぶこともある。

F は与えられた式をプログラムに変換する関数である。これにより、対象プログラムを操作するプログラムにおけるデータと対応付けることが可能となる。
ここでは、構文に対応するコンストラクタを用いて、ル式や式を生成する関数であるが、ここでは詳細を省略する。F から while 文やパターンマッチ文を生成する場合が欠落しているが、本論文では用いず、またほぼ if 文の場合と同じであるため、今回は省略している。

3. 1 表明の意味論
表明はラベル付き変数の状態に対して妥当かを判定する。意味論は図 4 のように定義されるが、以下の記法を用いている。

• σ はラベル付き変数に関する環境（ラベル付き変数から値への関数）である。

• E がラベル付きの式であるとき、E[σ] は各ラベル付き変数を σ によって値に置換した While 言語の式である。
 S [σ] も同様である。
l′′

′
 σ1 (x ) (if l = l )と定義する。
• σl1 ·σ2 (xl ) =  σ (xl′ ) (otherwise)2• σl は ラ ベ ル 無 し 変 数 に 関 す る 環 境 で あ り、
σl (x) = σ(xl ) とする。
意味論での記述に ϵ が用いられているが、これは空の環境である。実際には、E[σ] によって変数がすべて値に置換されているため、式の評価は環境の影響を受けず、任意の環境で良い。

v, σ ⇓E v

E1 , σ ⇓E n1x, σ ⇓E σ(x)E2 , σ ⇓E n2

E 1 , σ ⇓E v

E 2 , σ ⇓E v

E2 , σ ⇓E v2

E1 , σ ⇓E v1

v1 , v2

E 1 , σ ⇓ E n1

E2 , σ ⇓E n2

n1 > n2E 1 , σ ⇓ E n1

E2 , σ ⇓E n2n1 ≥ n2

E1 < E2 , σ ⇓B false

B2 , σ ⇓B true

B1 , σ ⇓B false

B1 and B2 , σ ⇓B true
B1 , σ ⇓B b1E 2 , σ ⇓E v

E1 <= E2 , σ ⇓B false

n1 < n2

E1 < E2 , σ ⇓B true
B1 , σ ⇓B true

v1 , v2

E1 <> E2 , σ ⇓B false

n1 ≤ n2E2 , σ ⇓E n2

E2 , σ ⇓E v2

E 1 , σ ⇓E v

E1 <= E2 , σ ⇓B true
E1 , σ ⇓E n1...

E1 = E2 , σ ⇓B false

E1 <> E2 , σ ⇓B trueE2 , σ ⇓E n2

E2 , σ ⇓E v2c(E1 , E2 , . . .), σ ⇓E c(v1 , v2 , . . .)E1 = E2 , σ ⇓B true

E 1 , σ ⇓ E v1E2 , σ ⇓E n2

E1 - E2 , σ ⇓E n1 − n2

E1 , σ ⇓E v1

E1 * E2 , σ ⇓E n1 ∗ n2

E1 , σ ⇓E n1

E1 , σ ⇓E n1

E1 + E2 , σ ⇓E n1 + n2

E1 , σ ⇓E n1b, σ ⇓B b

E 2 , σ ⇓ E n2

B2 , σ ⇓B false

B1 or B2 , σ ⇓B false

B2 , σ ⇓B b2

b1 か b2 の少なくとも一方が trueでない

B1 and B2 , σ ⇓B false
B1 , σ ⇓B b1

B2 , σ ⇓B b2

b1 か b2 の少なくとも一方が true

B1 or B2 , σ ⇓B trueB, σ ⇓B trueB, σ ⇓B false

not B, σ ⇓B false

not B, σ ⇓B true

skip, σ ⇓ σE, σ ⇓E v

S 1 ; S 2 , σ ⇓ σ2′

B, σ ⇓B false S 2 , σ ⇓ σ′if B then S 1 else S 2 end, σ ⇓ σ′S , σ ⇓ σ1S 2 , σ1 ⇓ σ2x := E, σ ⇓ σ[v/x]B, σ ⇓B true S 1 , σ ⇓ σ
B, σ ⇓B true

S 1 , σ ⇓ σ1if B then S 1 else S 2 end, σ ⇓ σ′B, σ ⇓B false

while B do S end, σ1 ⇓ σ2while B do S end, σ ⇓ σ2while B do S end, σ ⇓ σx, σ ⇓E ck (v1 , v2 , . . .) S k , σ[v1 /x1 , v2 /x2 , . . .] ⇓ σ′match x with | . . . | ck (x1 , x2 , . . .) => S k | . . . end, σ ⇓ σ′
図2

While 言語の意味論。σ は変数環境であり、変数から値への関数である。⇓E が式の評価、⇓B がブール式の評価、⇓ が文の評価をそれぞれ表す。

3. 2 ホーアの三つ組
Pg 、Qg をそれぞれ g のみをラベルとして持つ表明、
S を While 言語の文としたとき、{Pg } S {Qg } をホーアの三つ組（または単に三つ組）と呼ぶ。ホーアの三つ組と表明における構文としての三つ組を区別するため、後者を三つ組の表明と呼ぶ。
三つ組の意味論は、言語と表明の意味論を用いて以下のように定義される。
∀σ1 σ2 , σ1 |= Pg ⇒ S , σ1 g ⇓ σ2 g⇒

σ2 |= Qg|= {Pg } S {Qg }この記述は、図 4 における三つ組の意味論と非常に似ている。Pg と Qg は g 以外にラベルが出現しないため、表明の三つ組における意味論と同様の式と考えたとき、既存の環境である σ に依存した変数が現れない。この意味で、既存の環境を補うことで、両者を同一と見なせる。

EL::=SL::=

PL , QL

図3v|

xl (l ∈ L) ||

skip

A ||

x:=E

EL + ELS L ;S L||

EL - EL

match x with | c(x1 , x2 , . . .) => S | . . . end|

F (E L )b|

EL = EL|PL ∧ QL|f (E L )||EL , ELPL ∨ QL||

EL ≤ EL|

constr(E L , c) ||EL * EL

if B then S L else S L end|::=|

EL < EL|c(E L , E L , . . .)while B do S L end| ¬PL[{PL,l } S L {QL,l }]l (l < L)

表明言語の構文。L がラベルの列、E L がラベル付き変数を含む式、S L が変数を用いた文、PL が表明をそれぞれ表す。

σ |= trueE1 [σ], ϵ ⇓E v

E2 [σ], ϵ ⇓E v

E1 [σ], ϵ ⇓E v1

E2 [σ], ϵ ⇓E v2σ |= E1 = E2E1 [σ], ϵ ⇓E v1E2 [σ], ϵ ⇓E v2σ |= E1 neqE2v1 ≤ v2E1 [σ], ϵ ⇓E v1E2 [σ], ϵ ⇓E v2σ |= E1 ≤ E2σ |= Pv1 , v2
v1 < v2σ |= E1 < E2σ |= Q

σ |= P ∧ Qσ |= Pσ |= Qσ |= P ∨ Q

σ |= P ∨ Q

E[σ], ϵ ⇓E v

E[σ], ϵ ⇓E c(v1 , v2 , . . .)σ |= constr(E, c)′∀σ1 σ2 , σl1 · σ |= P⇒σ |= f (v)σ |= f (E)l′′S [σ], σ1 ⇓ σ2 l⇒′σl2 · σ |= Q′

σ |= [{P} S {Q}]l
図4

表明の意味論

意 味 論 は 反 転 補 題 が 成 り 立 つ こ と と 合 わ せ 、環4 推論規則

境を σ1 g [v1 /xi1 , v2 /xi2 , . . .] として S i を実行すると、ここでは、ホーアの三つ組のための推論規則を定義

σ2 g と い う 環 境 と な る こ と が 示 せ る 。こ の 環 境する。本論文で用いる規則は図 5 のように定義されは σ1 g [v1 /xi1 , v2 /xi2 , . . .] = σ1 [v1 /xi1 , v2 /xi2 , . . .] を満る。この中で Bl という表現を用いているが、これはた す。こ れ を σ = σ1 [v1 /xi1 , v2 /xi2 , . . .] と す る と 、B の中の変数にラベル l を付けたものである。

σg (x) = ci (v1 , v2 , . . .) かつ σg (xi j ) = v j となる。また、

gg

ggg

変数のラベルの付け外しがあることやパターンマッ

P には x1 , x2 , . . . は含まれないため、P[σ] = P[σ1 ] でチ構文のための規則は特徴的だが、その他は広く用いある。したがって、σ |= xg = ci (xi1 , xi2 , . . .) ∧ P を満たられている規則である。そのため、以下の健全性の証す。これらと帰納法の仮定から、σ2 |= Q を満たすこ明も、ほぼ通常のホーア論理の証明同様である。とが示される。

gg□

Theorem 4.1. 推論規則は健全である。つまり、⊢g{P} S {Q} ならば |= {P} S {Q} である。

5 推論による三つ組の取り扱い

証明 推論規則に基づく帰納法による。パターンマッ

実際にこの推論規則を用いて検証をする場合、問題チ以外については教科書通りであるため、省略する。

が存在する。図 5 に示した推論規則では、三つ組の表

パターンマッチに関しては、意味論側の前提と∨し て σ1 |= i∈{1,...n} constr(xg , ci ) が 成 り 立 つ た め 、明を示すために意味論を用いている。しかし、3. 2 節ある i が存在して、σ1 (x) = σ1 (x ) = ci (v1 , v2 , . . .)三つ組の意味論と同様であることから、三つ組の表明と な る 。ま た 、前 提 と し て σ1 と い う 環 境 か らが妥当であることを示すことは、少なくとも三つ組をパターンマッチ文を実行すると σ2 g となる。文の示すのと同程度に難しいことがわかる。

ggg

で述べたとおり、三つ組の表明に関する意味論はほぼ

P ⇒ P′⊢l {P′ } S {Q′ }Q′ ⇒ Q⊢l {P} skip {P}⊢l {P} S {Q}⊢l {P} S 1 {Q}⊢l {Q} S 2 {R}⊢l {P ∧ Bl } S 1 {Q}⊢l {P} S 1 ; S 2 {R}⊢l {P[xl 7→ E l ]} x:=E {P}⊢l {P ∧ not Bl } S 2 {Q}⊢l {P} if B then S 1 else S 2 end {Q}⊢l {P ∧ Bl } S {P}⊢l {P} while B do S end {P ∧ not Bl }llll∀i ∈ {1, . . . , n}, P does not contain xi1, xi2,...
⊢l {xl = ci (xi1, xi2, . . .) ∧ P} S i {Q}∨l⊢l {P ∧ i∈{1,...n} constr(x , ci )} match x with | . . . | ci (xi1 , xi2 , . . .) => S i | . . . end {Q}

図5

ホーア論理の推論規則

例えば 2 節で挙げた乗算の例では、while 文によるこれは意味論から明らかである。しかし、F (sg ) の後繰り返しによって、文を表すデータが繰り返しの中でろが複雑化した場合を考えると、次のような規則が可大きくなるが、文を実行した結果に関する不変条件を能であることが望ましい。
σ |= [{P} S {Q}]l⊢l {Q[σl ]} S ′ [σl ] {R[σl ]}記述し、それが不変条件であることを確かめることになる。実際に、nの初期値を N として、以下の三つ組を考える。

{ng = N ∧ 0 < ng } S {[{true} F (sg ) {xl = N ∗ 10}]l }読みやすさのために対象のプログラムは S としている。

S には while 文が含まれるため、意味論によってこの三つ組が成り立つかを議論することは現実的でない。推論規則を用いて while 文の範囲に限定すると、推論する三つ組は以下のようになる。ただし、pの等式に関しては定数であるため記述の都合上省略した。
{pg = . . . ∧ ng = N − 1 ∧ 0 ≤ ng ∧sg = assign_s(”x”, int(10))}
while . . . end{[{true} F (sg ) {xl = N ∗ 10}]l }ここで while 文の不変条件を次のようにする。
pg = . . . ∧ ∧0 ≤ ng ∧ [{true} F (sg ) {xl = (N − ng ) ∗ 10}]l
この不変条件を用いることで while 文の事前条件、事後条件については容易に導出できるため、while 文の本体についての推論を行う。代入文が連続しているので、最弱事前条件をもとに検証する式は以下の通りになる。
pg = . . . ∧ ∧0 < ng ∧ [{true} F (sg ) {xl = (N − ng ) ∗ 10}]l⇒ pg = . . . ∧ 0 ≤ ng − 1∧[{true} F (sg ); x := 10 {xl = (N − ng + 1) ∗ 10}]l
三つ組の表明以外は明らかであるため消去すると、[{true} F (sg ) {xl = (N − ng ) ∗ 10}]l⇒ [{true} F (sg ); x := 10 {xl = (N − ng + 1) ∗ 10}]lσ |= [{P} S ; S ′ {R}]l
ここで、Q[σl ] という記述は、l や内側に含まれるラベル以外のラベルが付いた変数について、環境 σ によって値へ変換するものである。これは、表明において意味論上示された三つ組と、推論による三つ組の妥当性を組み合わせて示すものである。この規則の妥当性は健全性から示されるが、現在の健全性では推論のラベルが g に限定されている。そのため、この規則の妥当性を示すには、ラベルを一般化し、表明に他のラベルの変数が出現しないことを言及した上で証明を行う。
この規則により、データとして構築された範囲を推論によって示し、変数を用いて表されている部分をまた、次のプログラムを考える。

match p with| seq_s(p1 , p2) =>match p2 with| assign_s (v, a) =>p := seq_s(p1 , assign_s ("a", a)end
end
これは、文として S ; x := E のような形をしたプログ
ラムを表すデータが格納された pに対し、パターンマッチで内部を見ることで、S ; a := E という形に変更するものである。つまり、初期の pに格納された元のプログラムで実行後に xに入る値を v とすると、変更後のプログラムでは実行後に aに入る値が v となる

これが成り立たない原因は、S ′ の事前条件 R をいくよう変更するプログラムである。

らでも強化できてしまうためである。

この検証時には、先ほどと同様に変数のまま扱われ体系の健全性という視点では、三つ組の表明を導る文（上で言う S ）について、aに代入する文を表す入した影響はほとんどないが、実際に検証を行う際データと連結する部分も問題となるが、もう一点、Sには、対象プログラムの具体化できた箇所の検証をに関する三つ組を導出しなければならないという問進めるために推論規則を用いたい。本論文では場当′題がある。プログラム全体を S として、次の三つ組たり的に導入すべき規則について述べたが、今後は、各構文に対して推論規則を利用可能にできるよう体を考える。
{[{true} F (pg ) {x = v}]l ∧ p = seq_s(P, assign_s(”x”, E))}系を定式化する。

S′{[{true} F (pg ) {a = v}]l }
ここでパターンマッチ文の推論規則を適用すると、代入文の前後で成り立たなければならない式は以下の通りである。
{[{true} F (P); x := A(E) {x = v}]l ∧ p1g = P ∧ ag = E}

p := seq_s(p1, assign_s("a", a){[{true} F (pg ) {a = v}]l }ただし、事前条件に存在した等式やパターンマッチ

6 関連研究
Berger らによる研究 [1] は、マルチステージ計算に基づくメタプログラミングにおけるプログラム論理の提案であり、操作するプログラムと操作されるプログラムが同一の言語であるという意味で本論文の目的に近いが、以下の点で異なる。

• 内部情報の書き換え。 Berger らの研究では、対で生成される等式のうち余分なものは消去している。

象プログラムにおける内部構造を観察、編集する

代入と事前条件の強化によって、[{true} F (P); x := A(E) {x = v}]l ∧ p1g = P ∧ ag = Eことはできない。 一方、本論文ではこれらが単⇒ [{true} F (p1g ); a := A(E) {a = v}]lを示せば良いことが分かる。等式を適用すれば、含意のに操作が可能である。 ただし、そのことからプ帰結部を示すには先ほどと同様、σ |= [{true}F (P){E =v}]l と ⊢l {E = v} a := A(E) {a = v} である。後者は単純な代入に関する推論とラベルの付け替えのみなので、前者に着目すると、含意の前提部に存在するのは複合文の三つ組であり、その一部のみを取り出したものが示すべき命題となる。

なる構造付きのデータであるため、言語内で自由ログラムの正当性を示す段階で適当なプログラムとなること、またはならないことを示す必要がある。

• 対象言語での最適化。 Berger らの研究が対象としている PCFDP では操作されるプログラムの簡約も操作するプログラムと同様に行える。 しかし本論文の手法はそういったことはサポートしてこれらを示すには、意味論を元に以下の規則のようにかける定理を示す必要がある。
σ |= [{P} S ; x := E {Q}]l

おらず、必要であればデータ構造における書き換えをプログラムとして実装する必要がある。
データを変換してコードを得るという観点で、本σ |= [{P} S {Q[E l /xl ]}]l
定理自体は容易に示せるため省略する。以上の推論と研究の手法に近いのは eval を持つ言語を対象としたから S ′ に関する三つ組が証明できる。

Charlton の研究である [2]。本研究との主な差異は、このように、推論と意味論の組み合わせを利用する

Charlton の研究では文字列を対象として、主にプログことで、既存の推論規則を用いた検証が可能となる。

ラムの生成に着目している点がある。本研究では、プ

ただし、先ほどの定理に関して、複合文を一般化した

ログラムは既にデータ構造によって表現されている以下の規則が成り立つことが望ましいが、一般には成ように前提を置いているため、本来は前段階として立しない。
|= {P} S ; S ′ {Q}

構文解析が必要である。一方で、Charlton の研究は、|= {R} S ′ {Q}|= {P} S {R}

文字列に対しての構文解析についても定義し、その正当性を示している。

Charlton の研究では、文字列の構文解析を推論規則側に置いており、データ構造などと混在させて考えるとして取り扱うため、コード生成のみだけではなく、編集作業も可能であることを示した。

ことが難しい。 また、構文解析を推論規則側で判定

将来課題として、本研究の用いている推論規則は、するため、生成されるプログラムの構造をプログラム編集作業に対してそれほど自由度がないため、規則を中で常に文字列として扱わなければならず、構造の一強化することが挙げられる。また、本論文では F に部を書き換えるなどの作業において、他の箇所の構関して基本的な要素として与えておりほぼ議論され造を破壊しないことを保証することが非常に難しい。ていないが、どのような関数が望ましいのかなどの性

逆に本研究に構文解析を導入するには、F に関して質について議論したい。特に、6 にも挙げた構文解析拡張すれば良いため、比較的容易である。この拡張をについて、F の拡張と F の関係性を議論することでさらに進め、構文解析部分に対応する操作プログラム行われる。また、この関係性を通じて構文解析を行うを記述、検証することで、操作プログラムの入力から操作プログラムを記述、検証する。

出力まで全体の検証が可能となると考えている。
参考文献

7 終わりに
本論文では、メタプログラミングのうち、対象のプログラムをデータとして保持し、そのプログラムを操作する場合について、検証する手法を提案した。
操作する側のプログラムが対象プログラムをデータ[1] Berger, M. and Tratt, L.: Program Logics for Homogeneous Meta-programming, Logic for Programming, Artificial Intelligence, and Reasoning - 16th International
Conference, Revised Selected Papers, Clarke, E. M. andVoronkov, A.(eds.), Lecture Notes in Computer Science,Vol. 6355, Springer, 2010, pp. 64–81.
[2] Charlton, N.: Reasoning about string-based runtime code
generation, Unpublished, (2011).