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

対話的修正と対象プログラムとの合成手法
森口 草介

高橋 和子

本論文では、Coq により検証した系と、それに対して対話的修正機構を用いて作成した修正部分を、合成して一つの系として得る手法を与える。Coq により行った証明に対して、修正をコマンドを通じて対話的に行う機構、対話的修正機構を提案した。この対話の結果として記述したコマンドの列を対話的修正と呼ぶ。
対話的修正は、明示的に修正箇所を指示するコマンドの他に、それらの影響を受ける箇所を機構が提示し、その場所に挿入する項を表現するコマンドから構成される。これは、修正対象の系の記述から分離されているので、管理が容易となるものの、系が単体で完結しないなど、可読性の観点からは望ましくない。これを改善するために、対象の系と対話的修正を合成することが考えられる。しかし、型の宣言や関数における修正箇所は比較的容易に発見できるものの、証明に関しては証明を表す項から発見していたため、コマンド列として記述される証明において、適切な修正箇所を発見することは難しかった。
本論文では、対象としている系の証明を、合成が容易となるように変形することで、元の証明を利用して記述した対話的修正との合成を可能とする。変形の結果、元の証明に比べ記述量が増大してしまうが、これは自動化された箇所が一部展開されることに起因する。変形は元の証明の流れに合わせて行われるため、メンテナンス性や速度の観点では問題とならない。ここでは、小さな例を用い、合成時に発生しうる問題や変形方法について述べる。

ことなく解決したようにみえる場合がある。ただし、

1 はじめにその検証が意図した通りに行われたかを判断するこ

Coq をはじめとした対話的証明支援系による数学とは難しく、実際に検証しようとした仕様が意図を満的体系やプログラムの検証は、厳密な記述により確か

たさない場合もある。

さが保証される。他方、この厳密さにより、通常の手

対話的修正機構 [6] は、このような修正時における、による検証に比べ、記述の冗長さ、証明の煩雑さが発影響の範囲を網羅的に調べながら対象の修正を行う

生する。

ための機構である。この機構は、コマンドを通じた対この厳密さによる問題は、単純な拡張に対する再話により、一度記述した型や関数、証明に関する修正検証においても発生する。数学的体系における（表現を行う。修正の内容を機構が受け取ることで、影響を可能な）定数の追加やプログラミング言語における受ける範囲を調べ、提示し、修正を求める。この対話

糖衣構文の追加は、追加前に確かめた性質をほぼそによって見落としやすい修正箇所などを確実に提示すのまま満たす。この場合、自然言語による証明では、ることが可能となる。

拡張後の性質について「同様に」という言葉で記述す

以下、対話的修正機構を用いて修正する対象を被修ることも少なくない。しかし、Coq を用いた検証にお正系、作った修正の記述を対話的修正と呼ぶ。対話的

いて、「同様に」という記述は難しく、自動化を試す、

修正は、コマンドの列として記述され、被修正系から類似した証明を読ませる、などを試すにとどまる。一は分離されているため、修正内容の着脱が容易である

方で、自動化の手法によっては、一見検証を変更するという利点を持つものの、どの箇所がどのように変更されたかを確認することが難しいという問題を持つ。

A method for weaving an interactive extension into its target
Sosuke MORIGUCHI and Kazuko TAKAHASHI, 関西学院
大学, Kwansei Gakuin University.

第一著者はこの問題に対して、対話的修正と被修正系を合成することで問題の解決を図った [5] が、しかしこの時点では二つの問題によって全面的な解決に至らなかった。

ありうる。

• repeat内部に挿入する。この場合、繰り返しの

1. 修正する箇所が表面的な記述と無関係に行われ中で他の証明に影響を与えないために、可能な限るため、その位置を正確に計ることが困難だった。

り挿入内容を修正箇所以外で実行されないよう

2. 証明の記述を複雑化できるため、修正の適用方法が容易には決定できなかった。

に保護しなければならない。

• repeatの直後に挿入する。この場合、他の証明

前者は、特に証明を表すスクリプト（以下証明スクリがこの修正により影響を受けないよう、修正箇所プト）において顕著である。これは当初の対話的修正にのみ適用されるようにその箇所に現れるゴー

機構が、型と項の構造を元に修正箇所を決定し、証明

ル数を決定し、分岐を生成する必要がある。

スクリプトを利用することなく行っていたためであどちらの問題も、単一の repeatであれば解決も難しる。そのため、本来の証明の流れでは発生しない箇所

くないが、Coq では repeatをネストして使用できる。

に修正箇所が存在する、単一の tactic が生成した項のこれは、汎用に用いることを考えたとき、先ほど挙げ一部を修正箇所として検知する、といったことが発生た問題のどちらも常に考慮しなければならないことした。これにより、証明スクリプトのどの箇所から発を意味する。

生したかを決定することが難しく、また決定できたと

本論文では、この問題に対し、元の証明を再実行す

しても元の tactic がどのように振る舞うのかを見積もる際の動きを元に証明スクリプトを変形、展開し、挿ることが難しかった。

入する箇所を一意に特定することで解決する。その際この問題は、第一著者の提案した、記述された元のに、repeatなどの構文をできる限り変形しないままに証明スクリプトを再実行することで修正箇所を減ら合成をすることで、自動化を維持することを目標とす技法 [3] を用いることで解決できる。再実行では、する。

その証明スクリプトの流れに沿った修正箇所を得ら

本論文の構成は以下の通りである。

れ、またそのときに得られる修正箇所は tactic から実• 第 2 節では、対話的修正機構による修正の流れ際に出現するものであるため、これらの問題が回避さとその結果得られる対話的修正について述べたれる。

後、被修正系と対話的修正の合成において発生す後者の問題は、この手法でも未解決の問題である。
これは例えば以下のスクリプトを考える。
inversion H; destruct n; auto.

る問題を説明する。

• 第 3 節では、被修正系の証明スクリプトにおいて、修正の記述時に開始した点である挿入点について議論、分析をする。

修正によって、inversionの結果現れるゴールが変わり、autoによって証明できないものが現れうる。しかし、この場合で存在しない、などの理由によりdestructが失敗すると、再実行に基づく修正箇所の検出ではその位置から修正を開始する。この修正• 第 4 節では、被修正系の証明スクリプトを、挿入点の近辺において展開を行う。この作業により、合成を容易な手順とする。

• 第 5 節では関連研究に関して述べ、最後に第 6節においてまとめる。

結果を、上のスクリプトと合成しようとした場合、destruct nに対して位置、内容を決定しなければならない。しかし、これらが repeatによって繰り返されるように記述されていた場合、destruct nの失敗は修正によって増えたゴール以外でも発生している可能性がある。
この場合に修正をどこに挿入するかは、次の二つが2 対話的修正と合成の問題
対話的修正単体については、特にメンテナンス性に関する問題がいくつか存在する。ここでは、対話的修
正機構による修正の流れと、問題点について明らかにする。

2. 1 対話的修正機構
対話的修正機構とは、被修正系に対する修正を確実に行うために提案した機構である。そのため、ここでInductive exp : Set :=| val : Z -> exp| var : V -> exp| add : exp -> exp -> exp.

は単純な被修正系と修正について、例を用いて説明する。なお、本論文で扱う対話的修正機構は [3] において提案したものである。したがって対話的修正機構の挙動に関する形式的定義、詳細はそちらを参照されFixpoint eval (e : exp) (env : V -> Z) :=match e with| val z => z
| var v => env v| add e1 e2 => eval e1 env + eval e2 env
end.

たい。
被修正系の例として、簡単な変数付きの算術式について説明する。内容を箇条書きにしたものが以下の通りである。

• 算術式には定数、変数、加算がある。
• 評価は変数の値を持つ環境を引数に、算術式の構造に対して再帰的に評価することで行われる。

• 定数同士の加算を折りたたむ最適化がある。
• 算術式が変数を含む、という述語がある。
• 変数を含む算術式は、最適化しても定数にならないという証明がある。
これを Coq のコードとしたものが図 1 である。算術式や述語の定義が型として定義されており、また評
価と最適化が関数として記述されている。また、証明は述語に関する帰納法を用いている。
この証明は、図 1 以外に図 2 や図 3 のようにも書ける。各証明では、inductionによって述語に関する帰納法を行った際に三つのゴールに分離している。元のコードにおける証明では、一旦ピリオドで区切る
ことによりそれぞれの証明を順次行っていたが、図Fixpoint opt (e : exp) :=match e with| add e1 e2 =>match opt e1 with| val z1 =>match opt e2 with| val z2 => val (z1 + z2)| e2 ’ => add (val z1) e2 ’end
| e1 ’ => add e1 ’ (opt e2)end| _ => eend.
Inductive var_ include : exp -> Prop :=| var_v : forall v, var_ include (var v)| var_al : forall e1 e2 , var_ include e1 ->var_ include (add e1 e2)| var_ar : forall e1 e2 , var_ include e2 ->var_ include (add e1 e2 ).
Goal forall e, var_ include e ->forall z, opt e <> val z.
intros e H.
induction H; intros z; simpl .
intro vi; simpl in vi; inversion vi.
case_eq (opt e1 ); intros ; intro H1;
try ( inversion H1; fail ).
apply ( IHvar _ include z0 ); auto.
case_eq (opt e2 ); case (opt e1 ); intros ;intro H1; try ( inversion H1; fail ).
apply ( IHvar _ include z1 ); auto.
Qed.

2 のコードでは simplの直後にゴールが三つ残っており、それぞれに対して|で区切ったそれぞれを適用す

図1

Coq による単純な算術式についての検証。

ることを明示している。この場合、述語の定義の変化などによりゴールの数が変化すればそこで証明が止えるものは、単項の負号である。対話的修正機構でまるため、信頼性の向上に役立つと考えられる。

は、コマンドにより型の拡張を行うと、その後関数や他方、図 3 ではそれぞれのゴールに一つずつ適用

証明に対し修正を指示され、それをコマンドによってすることと異なり、三種類の||を使って区切った証明

修正するという流れとなっている。例えば図 1 を対象を順次試すように記述されている。この場合、加算にとした場合、図 4 の対話的修正が記述できる。 被修関しての証明である二番目と三番目が、例えば乗算を正系の証明を図 2 や図 3 に入れ替えた場合、表面的組み込んだ場合の証明としても利用できる。このように記述する対話的修正は変化しない。しかし、これはに、証明としてはある程度先の修正を見越した記述も原因が異なっている。

ありうる。
ここで、算術式の演算子の追加を考える。ここで考• 図 1 では inductionによって生成されたゴールがそのまま残ったため、そのゴールについて証明をGoal forall e, var_ include e ->forall z, opt e <> val z.
intros e H.
induction H; intros z; simpl; [intro vi; simpl in vi; inversion vi |case_eq (opt e1 ); intros ; intro H1;
try ( inversion H1; fail );apply (IHvar _ include z0); auto |case_eq (opt e2 ); case (opt e1); intros ;intro H1; try ( inversion H1; fail );apply (IHvar _ include z1); auto ].
Qed.

図2

証明の別解 1。

Goal forall e, var_ include e ->forall z, opt e <> val z.
intros e H.
induction H; intros z; simpl;(intro vi; simpl in vi; inversion vi;fail) ||
(case_eq (opt e1 ); intros ; intro H1;
try ( inversion H1; fail );apply (IHvar _ include z0); auto; fail) ||(case_eq (opt e2 ); case (opt e1); intros ;intro H1; try ( inversion H1; fail );apply (IHvar _ include z1); auto ).
Qed.

Extend Inductive exp : Set :=| neg : exp -> exp.
Extend Inductive var_ include : exp -> Prop:=
| var_n : forall e, var_ include e ->var_ include (neg e).
Deploy .
(∗ eval ∗)exact -(eval e0 env ).
Defined .
(∗ opt − o u t s i d e ∗)exact ( match opt e0 with| val z1 => val (-z1)| e’ => neg e’end ).
( ∗ o p t − i n s i d e −add1 ∗ )exact (add (neg e0) (opt e2 )).
( ∗ o p t − i n s i d e −add2 ∗ )exact (add (val z1) (neg e0 )).
Defined .
(∗ proof ∗)case_eq (opt e); intros ; intro H1;
try ( inversion H1; fail ).
apply ( IHvar _ include z0 ); auto.
Qed.

図4

負号に関する対話的修正。

メリットとなる。
図3

証明の別解 2。

本論文における目標は、対話的修正と被修正系を合成し、修正後の体系を表すソースコードを生成す求めている。

• 図 2 では適用するゴールの数が修正結果生成されるゴールについて無視する必要があったため、追加生成されたゴールを別途証明を求めている。

• 図 3 ではそれぞれ||でつながれた証明を試行し、結果的に失敗したためそこまでの状態で別途証明を求めている。

ることである。この場合に発生しうる問題としては、以下のものがある。

1. 修正時に作成した記述を埋め込む場所の発見が難しい。

2. 発見した箇所に埋め込んだ場合に他の証明に影響を与える可能性がある。

3. 可読性や自動化をある程度保った状態にすることが難しい。

2. 2 対話的修正の問題順に説明する。

対話的修正機構では、被修正系に対して網羅的な修

まず、発見の難しさは、対話的修正機構の修正箇所正を求めることで、意図せぬ修正漏れを起こしづらくの発見手法に依存する。当初、対話的修正機構によるする。また、図 1 と図 4 のように、対話的修正の記

証明内の修正箇所は、証明を表す項を関数同様に調べ

述が被修正系と分離されているため、被修正系への適ることで行っていた。これは網羅性や確実性、既存の用と分離が容易に行えるという利点がある。

システムの再利用、理論的基礎という視点では優れて一方で、分離されてるために型の宣言などの全体いるが、項における修正箇所が証明スクリプトの修正を把握することが難しくなる。これは被修正系と分に比べ過剰に検出されることから、ユーザビリティの離されていることとのトレードオフとなっているが、低下を招いていた。また、修正箇所がどのような流れ

修正の内容を特に分離する必要がない場合、単純なデによって発生したかが分かりづらく、本研究のように証明スクリプトと修正箇所の対応付けが必要となるT際の障害となっていた。

::=

atomic tac

|

T; T

現在では、再実行に基づく修正箇所の発見 [3] を利|T || T

用することで、証明スクリプトに利用された tactic の|

T ; [T |T |...|T ]単位で修正箇所を判定できる。そのため、本論文では|try(T )

修正そのものがこの手法に基づいて行われた前提で議論を進める†1 。

|

repeat(T )次に、他の証明への影響を考える。Coq において証図5

本論文で扱う Ltac（のサブセット）。

明に用いられる言語 Ltac は repeatによる繰り返しや

図 5 の文法を Ltac の文法として用い、証明スクリプ

tactic の連結、複数の特定数のゴールへの適用などのトを要素 T の 0 個以上のリストとして扱う。

機能がある。修正によって repeatの中で新しいゴー

ここで表す文法は以下のような分類である。

ルが生成されると、その直後に何らかの形で修正の内• atomic_tacはこれ以上分解できない tactic を表

容を配置する必要がある。しかし、その修正は他の繰

し、T1;T2は T1に続けて T2を実行することを表す。

り返しにおいて影響を与えうる。一方、特定数のゴー• T1 ||T2は T1を実行し、失敗した場合に T2を実ルへの適用は数が変化しているため、必ず変更しなけ
ればならない。
最後に可読性や自動化について考える。上の二点について解決しうる最も単純な手法は、証明に使われている記法を全て展開し、単一の tactic を必要なだ行する。

• try(T)は Tを実行し、失敗した場合は何も実行しなかったものとする。

• repeat(T)は Tを、失敗するまで繰り返し実行する。

け配置するものである。例えば、上の repeatについなお、この中に含まれていない Ltac の文法は全てて、それが 3 回繰り返したのであれば、3 回その中身

atomic_tacとして扱う。

を記述する、tryなどについては成功した場合中身を対話的修正において、修正を行う起点を以下では挿置き、失敗した場合は消去する、などの手法で達成で入点と呼ぶ。挿入点は対話的修正機構がどのような点きる。しかし、この場合「類似の証明に対して自動的を開始点にするかによって異なる。

に証明する」などの工夫を施した記述が全て展開され

現在提案している対話的修正機構の再実行機能は、ており、それ以降対話的修正機構が対応できないよう

連結の途中における失敗、特定数のゴールへの適用まな修正を行った場合に再利用することが困難となる。

たは tactic の終端まで再実行を行う。この結果、多く

本論文において述べる手法は、元の記述の構成をの場合は repeatや tryの内部に挿入点は存在しない。

極力保持したままで修正を合成する。この手法では、

これは、repeatは内部で失敗するまで終了しないが、まず証明スクリプトを一部のみ展開し、挿入すべき

失敗した場合にエラーにならずに終了するため、再実箇所を決定可能にする。展開は汎用的なものでなく、行の手法の関係上以降の tactic の実行を続けようとす

対象とする対話的修正についてのスクリプトの挙動るためである。

を元に行う。これにより、最小限度の展開によって合成が可能となることが期待できる。

例外として、特定数のゴールへの適用時に中止する場合がある。したがって、以下のようなコードを記述した場合、挿入点が repeatの内部に存在する場合が

3 挿入点

発生する。

展開のために、ここでは各ゴールがどのようなス

repeat ( inversion H; [ .. | .. ])クリプト内のパスを通過するかを考える。以下では、Hの型が帰納的であり、かつコンストラクタを追加し†1 前述の通り、2. 1 節の説明はこの機能を用いている。

た型である場合、生成されるゴールが増える可能性

がある。しかし、このコードは可読性やメンテナンス性に関して疑問がある。なぜならば、繰り返し同じも

容はその分岐が終了した後に増加したゴールを証明する箇所に配置する。

のを展開し、同じ処理をすることはほとんどないた

3. 挿入点が特定数のゴールへの適用内部の場合、めである。例えば destructのように同じ変数名で異後続の tactic の列を上と同様にして内部に組み込なる変数が割り当てられるようになる場合もあるが、み、その後外側の適用を展開する。具体的には、

repeatで繰り返すほど同じ処理として記述することは各ゴールに適用する tactic の列をその順序に合わ

難しく、省略した分岐のそれぞれが比較的複雑な記述

せて配置する。

をする必要がある。このような場合、可読性に関して

この展開は挿入点以外について行われないため、前節の問題の他に、対話的修正機構の範囲に限らず修正一において説明した対話的修正機構の特性上、特定数の般に対して非常にもろい構造となる。

ゴールへの適用が含まれない自動化はそのまま残る。

本論文では、挿入点が構造的に内側に入るものを展開する。この構造とは、repeatや tryの他、||でつ
ながれたものや特定数のゴールへの適用を意味する。
これらはゴールが増加した際に成功や失敗について
様々な影響が考えられるため、展開することで調整可能とする。

この展開を再帰的に行うことで、挿入点は次の三点のどれかとなる。

• 二つの tactic の間。この場合は単純にその間に修正結果を挿入すればよい。

• 二つの tactic を連結した間。後続の tactic 全体をtryで囲い、tactic 終了後に修正内容を配置することで合成できる。

4 証明スクリプトの展開
前節の分析から、次の展開を考える。

• ||の右側の内部。これは直上の基準同様に連結した後続の tactic に tryを用いることで合成できる。

1. 挿入点が repeat、tryの内部である場合、また

なお、この挿入では tryの追加が発生するので、そのは||によって連結したものの左側の内部である場

ほかの挿入点がこれによる影響を受ける場合、再度上合（右側の内部に挿入点がある場合は除く）、以

に挙げた展開を行う必要がある。

下の方針で展開する。まず、複数のゴールで実行

展開を図 1 の証明スクリプトに適用すると、全くされないように直前で tactic の連結を切り、適用

変形されない。これは、挿入点が最後の Qedの直前でされるゴールの数だけ複製する。その後、あり、展開する必要がないためである。挿入後の証明• repeatは被修正系や対話的修正における繰
り返しの数だけ、生成されるゴールの数に合わせて繰り返しリストに挿入する。

• tryの内部の tactic について、成功失敗によ
り中身をそのまま置くか除去するかを決定する。

• ||の左側が成功する場合は左側のみを、右側について試す場合は右側を残す。

2. 挿入点が特定数のゴールへの適用直前の場合、後続の tactic の列を内部に組み込む。これは各々

スクリプトは以下の通り。
Goal forall e, var_ include e ->forall z, opt e <> val z.
intros e H.
induction H; intros z; simpl .
intro vi; simpl in vi; inversion vi.
case_eq (opt e1 ); intros ; intro H1;
try ( inversion H1; fail ).
apply ( IHvar _ include z0 ); auto.
case_eq (opt e2 ); case (opt e1 ); intros ;intro H1; try ( inversion H1; fail ).
apply ( IHvar _ include z1 ); auto.
case_eq (opt e); intros ; intro H1;
try ( inversion H1; fail ).
apply ( IHvar _ include z0 ); auto.
Qed.

のゴールへ適用する tactic に対し、証明がその分岐内で終わっていれば何もせず、終わっていなけ
れば後ろの tactic の列をそのまま連結する。その後、特定数のゴールへの適用に増加したゴールの数だけ idtacを適用するように追加する。修正内

次に図 2 に対して行った場合に記す。

Goal forall e, var_ include e ->forall z, opt e <> val z.
intros e H.
induction H; intros z; simpl; [intro vi; simpl in vi; inversion vi |case_eq (opt e1 ); intros ; intro H1;
try ( inversion H1; fail );apply (IHvar _ include z0); auto |case_eq (opt e2 ); case (opt e1); intros ;intro H1; try ( inversion H1; fail );apply (IHvar _ include z1); auto |idtac ].
(∗ i n s e r t the s c r i p t here ∗)5 関連研究Coq における証明のように、tactic を用いた証明に関するリファクタリングは、Whiteside らが行った研究がある [4]。この研究におけるリファクタリングは、
名前の変更などの比較的局所的なものと、証明をゴー
ル指向から演繹的証明に変更するなどの大域的なものがあり、可読性に重点を置いている。しかし、本研究で述べたように修正や挿入を意識した変形や展開でこの場合の挿入点は [の直前であり、上で述べた展開はないため、これらのリファクタリング技法をそのまの手順の 2 に相当する状況である。そのため、エラー

ま用いることはできない。今後、このリファクタリン

を回避するために idtacを追加することでゴールの数

グ技法による証明スクリプトの変形が、どのように本を合わせている。また、後続の tactic の列が存在しな論文で提案した手法に影響を与えるかを分析するこ

いため、それぞれの記述はそのままである。

とで、本論文の手法の拡張として導入を考慮したい。

最後に図 3 に対して展開を行った場合について述

本研究では、tactic の個々の挙動をほぼ考慮せず、べる。この場合の挿入点は二つ目の||の直後であり、意味については一部の文法のみを考慮するに留めて再実行は case_eq (opt e2)の変数名が存在しないといるが、各 tactic の挙動について考慮することで、そいうエラーによって止まっている。これは展開に相当の他の展開の基準を得ることも考えられる。Ltac のする状況ではない（||の内部だが、右側なので例外的意味論としては、Jedynak らの研究 [1] がある。今後に許される)。したがって、展開せずに、一部変形をはこれを用いたより詳細な分析、展開について考慮し行って挿入を行う。挿入の方法を元に生成される証明た手法の提案や、今回の展開が Ltac における意味論

スクリプトは以下の通り。

に関して意味を保存していることの証明を行う。

Goal forall e, var_ include e ->forall z, opt e <> val z.
intros e H.
induction H; intros z; simpl.
(intro vi; simpl in vi; inversion vi;fail) ||
(case_eq (opt e1 ); intros ; intro H1;
try ( inversion H1; fail );apply (IHvar _ include z0); auto; fail) ||(∗ tr y i s i n s e r t e d ∗)(try (case_eq (opt e2 ); case (opt e1);
intros ;intro H1; try ( inversion H1; fail );apply (IHvar _ include z1); auto )).
(∗ i n s e r t e d s c r i p t ∗)case_eq (opt e); intros ; intro H1;
try ( inversion H1; fail ).
apply (IHvar _ include z0); auto.
Qed.

分離したプログラムの断片を一つのコードとして表現することは、アスペクト指向 [2] における織り込みやメタプログラミングとして行われる。しかし、多くのアスペクト指向の織り込みやメタプログラミングは
コンパイル時や実行時において想定した動作を実現するものであり、それらの機能を組み込んだソースコー
ドを生成することはほとんどない。これは、機能、非機能にかかわらず、これらの記述を内部に組み込んだ記述が必ずしも元の言語における記述と対応せず、また対応する場合でも可読性の確保は難しいためである。本研究の基盤である対話的修正機構は、そもそも保守的な変更に限っているため、元のソースコードのこのように、順次試行することによる自動化は残す

構造を保持しつつ、可読性の確保が可能となった。

ことができており、これに乗算を追加した場合でも証明が自動的に行われる。しかし、tryが追加されたこ

6 まとめとにより、他の修正点が try内部に存在した場合の問

本論文では、対話的修正機構によって行った修正を題が発生しうる。この場合、スクリプトが複雑化した

被修正系に組み込むための手法として、被修正系の証

り、自動化が展開される可能性がある。

明スクリプトを展開を経て行う手法を提案した。この手法では、単純な合成ではうまく挿入できない修正のれる。

記述を、被修正系の記述を展開することで可能としこれをサポートするには repeat内など、全ての通た。繰り返しなどの自動化については挿入しなければ過した箇所や通過時の状態を計算し、展開方法をさならない箇所に限り展開することで、少なくとも簡単

らに拡張する必要がある。しかし、これによって自動な例では残すことに成功している。

化を全て展開しなければならない可能性もあるため、今後の課題としては、挿入点の拡張が挙げられる。
本論文における手法は、対話的修正機構の再実行機能

今後は自動化の残り方や柔軟な展開手法について考察する。

がエラーを起こす箇所まで実行することを利用した。
しかし、この再実行機能は必ずしも外側まで実行せ

参考文献

ず、修正によって発生したゴールが生成された tactic[1] Jedynak, W., Biernacka, M., and Biernacki, D.: An operational foundation for the tactic language of Coq, PPDP,
Peña, R. and Schrijvers, T.(eds.), ACM, 2013, pp. 25–36.
[2] Kiczales, G., Lamping, J., Menhdhekar, A., Maeda,
C., Lopes, C., Loingtier, J.-M., and Irwin, J.: AspectOriented Programming, 11th European Conference on
Object-Oriented Programming, LNCS, Vol. 1241, June
1997, pp. 220–242.
[3] Moriguchi, S. and Watanabe, T.: An interactive extension
mechanism for reusing verified programs, Proceedings ofthe 28th Annual ACM Symposium on Applied Computing,
SAC ’13, New York, NY, USA, ACM, 2013, pp. 1236–
1243.
[4] Whiteside, I., Aspinall, D., Dixon, L., and Grov, G.: Towards Formal Proof Script Refactoring, Proceedings of the
18th Calculemus and 10th International Conference on Intelligent Computer Mathematics, MKM’11, Berlin, Heidelberg, Springer-Verlag, 2011, pp. 260–275.
[5] 森口草介, 渡部卓雄: Coq のための対話的修正機構を用いた変更の織り込み手法, 日本ソフトウェア科学会 第28 回大会, September 2011.
[6] 森口草介, 渡部卓雄: 定理証明支援系 Coq への対話的修正機構の導入, 情報処理学会論文誌プログラミング（PRO）, Vol. 5, No. 4(2012), pp. 27–38.

で実行を止めた方がよい場合もある。これは、生成後から外側に脱出するまでに、不可逆な tactic が実行された場合などがある。極端な例として、clearという

tactic は、環境で使用出来る変数を消去するものであり、一般には以降使用しない変数に対して用いること
で環境を整理する目的に使用される。しかし、変数が見えなくなるためこれを実行した後で証明ができな
くなることもある。
このように、可能な限り tactic を実行するという戦
略は、場合によっては問題を起こしうる。調査した範囲ではこのように過剰な操作が行われることはなかったが、想定することは可能であり、そのための対策を用意すべきである。現在、実装する上で出現箇所に戻るコマンドの提供を考えている。この場合には、挿入点が任意の箇所に入ることになり、現在の仮定が崩