/************************************************************************/ /* Kima -- KL1 プログラム自動修正系 (version 2.200) */ /* */ /* March 2002 */ /* */ /* 網代育大 上田和紀 */ /* */ /* 早稲田大学大学院理工学研究科 */ /* 早稲田大学理工学部情報学科 */ /* */ /* {ajiro,ueda}@ueda.info.waseda.ac.jp */ /* */ /* Copyright (C) 1999-2002 Yasuhiro Ajiro, Kazunori Ueda */ /* */ /************************************************************************/ 1. 概要 Kima は静的解析によって KL1 プログラム中の変数の書き誤りを自動的に修正する ことができます。これは非常に限定的に聞こえますが、KL1 などの(並行)論理型言 語ではプログラム中に変数を多用するため、簡単な誤りの多くは変数の使い方の間 違いによって発生します。また、変数の書き誤りのような単純な誤りでない場合で も、Kima は誤りの原因となっている場所をプログラムテキスト中の一定の範囲内 に絞り込むことが可能です。ただし、すべての誤りが検出/修正できるわけではあ りません。 Kima は、大きく分けて次の3つのプロセスで自動修正を行ないます。すべてのプロ セスにおいて、モード/型解析が基本的な役割を果たします。 (1) モード/型解析による誤りの検出 (2) モード/型制約集合の矛盾する極小部分集合および検出規則に違反する変数 記号の計算による誤り箇所の特定 (3) 特定した怪しい変数記号に基づく修正案の探索と求めた修正案への優先度づけ 詳細については文献[1-4]を参照してください。 1.1 静的解析による誤りの検出 KL1 におけるモード/型解析は、プログラムテキスト中の関数/定数/変数記号出現 と制約規則から得られる制約式の集合を制約充足問題として解くもので、プログラ ムサイズに関してほぼ線形の手間で行なうことができます(文献[6,7])。このモー ド/型制約の集合が充足可能なプログラムを well-moded/typed なプログラムとい い、充足不可能になるプログラムを ill-moded/typed なプログラムといいます。 プログラム中に誤りが存在する場合は、プログラムテキストから得られるモード/ 型制約式の集合が充足不可能になることが多いため、誤りの多くを静的に検出する ことが可能です。 1.2 誤りの候補の特定 モード/型制約式の集合が充足不可能となる場合、制約式集合の中から矛盾する極 小部分集合(minimal inconsistent subset)を求めることで、誤りの原因の候補を プログラム中の一定の範囲内に絞り込むことができます(文献[5])。これは、モー ド/型制約がプログラム中の記号出現に対して課されるため、矛盾の原因となって いる制約(の候補)を特定することで、それを課している節と記号を誤りの原因(の 候補)と見なせるからです。 実験では、モードと型を併用した場合、1箇所の誤りに対する誤りの検出率は 70% 程度です。そこで Kima は、モード/型以外に以下の「検出規則」を設けて検出力 の強化を図っています。 [検出規則 1] - ガードで検査している変数がへッドにもなくてはならない - ユニフィケーションの両側に同一の変数が出現してはならない (部分的な occur-check) [検出規則 2] - singleton 出現している変数の名前は，下線 `_' で始まっていなければ ならない Kima は常に「検出レベル1」を仮定します。検出レベル1では、検出規則1のみが用 いられます。検出規則1を用いずに解析を行なうことはできません。コマンドライ ンオプションによって、「検出レベル2」が指定できます(第4節参照)。検出レベル 2では、検出規則1と2の両方が用いられます。実験では、検出規則1と2を用いるこ とで検出率が 90% 以上に向上しました。言い換えれば、検出規則に規定されたプ ログラミングスタイルを守ることで、90% 以上の誤りが自動的に検出されるという 「恩恵」を受けることができます。 1.3 軽微な誤りの自動修正 矛盾する極小部分集合によって怪しいと指摘された制約は、 - それを課す原因となっている記号を他の記号に書換えるか、あるいは - 記号が変数記号である場合は、同一節中の他の記号出現を書換えて、 その変数記号の出現数を増やす ことによって変化し、矛盾が解消する可能性があります。Kima は well-moded/typed なプログラムを「正しい」プログラムとみなし、怪しいとされる変数記号の書換え と書換え後のプログラムのモード/型検査を機械的に行う(generate-and-test)こと によって修正案を探索します。前述の矛盾する極小集合を用いて誤りの候補を絞り 込むことにより、探索を現実的な時間で行うことができます。詳細については文献 [1-4]を参照してください。 モード/型検査による修正案は一般に複数求まるため、Kima は以下のヒューリス ティクスを使って、求めた修正案に優先度をつけます。 <優先度づけのためのヒューリスティクス> [ヒューリスティクス1] 節中において、ある変数が (a) singleton (1回のみ)出現 (b) へッドに2回以上出現 (c) へッドまたはボディに3回以上出現 (d) ある述語呼び出しの引数に2回以上出現 しているようなものは、もっともらしくない。 [ヒューリスティクス2] リスト自身とその要素の型が同じ、すなわち、プログラム中のある節において パス p と要素のパスp<.,1> (非空リストの第1引数目) に同一の変数が出現し ている場合はもっともらしくない。 具体的には、修正案中のヒューリスティクスに合致する部分に対して規定のペナル ティを課します。その結果、より少ないペナルティをもつ修正案を、よりもっとも らしい案とみなします。各ヒューリスティクスに対応するペナルティ値については heuristics.kl1 中のコメントまたは文献[3]を参照してください。 2. 使用法 Kima の実行は、修正したい KL1 プログラムのソースファイルを次のように指定す るだけです。ファイルは複数指定できます。 % kima xxx.kl1 yyy.kl1 zzz.kl1 これによって、モード、型、および検出レベル2を用いた深さ1の探索による修正案 のうち、もっとも優先度の高いものが提示されます。 誤り箇所の特定のみを行ないたい場合は、次のように指定します、 % kima +mis xxx.kl1 yyy.kl1 zzz.kl1 これにより、モード/型制約の矛盾する極小部分集合と、検出規則に違反する変数 記号が出力されます。誤りが発見できなかった場合は、なにも出力されません。 探索の深さの指定など、細かい実行制御については第4節を参照してください。 3. 実行例 例 1: 1 箇所の誤り 2つのリストをつなげる append プログラムの変数を1箇所書き間違えている例を 考えます。 +------- append.kl1 ---------------------------------------------------+ | | | :- module test. | | | | append([], Y,Z) :- true | Y=Z. | | append([A|Y],Y,Z0) :- true | Z0=[A|Z], append(X,Y,Z). | | % X <-- correct | | | +----------------------------------------------------------------------+ これに対し、優先度100までの修正案を提示するには次のようにします。 % kima +p 100 append.kl1 すると次の出力が得られます。 ================= Suspected Group 1 ================= ------------- Priority 1 ------------- append([A|Y],X,Z0):-true|Z0=[A|Z],append(X,Y,Z). in test:append/3, clause No.2 ----- append([A|X],Y,Z0):-true|Z0=[A|Z],append(X,Y,Z). in test:append/3, clause No.2 ----- ------------- Priority 2 ------------- append([A|Y],Y,Z0):-true|Z0=[A|Z],append(Z0,Y,Z). in test:append/3, clause No.2 ----- ------------- Priority 3 ------------- append([A|Y],Y,Z0):-true|Z0=[A|Z],append(A,Y,Z). in test:append/3, clause No.2 ----- append([A|Y],Y,Z0):-true|Z0=[A|Z],append(Z,Y,Z). in test:append/3, clause No.2 ----- append([A|Y],Y,Z0):-true|Z0=[A|Z],append(Y,Y,Z). in test:append/3, clause No.2 ----- これは、優先度1から3までの6つの修正案が求まったことを示しています。優先度1 の修正案が最も優先度の高い修正案です。修正案はひとつずつ `-----' で区切ら れて表示されます。`in test:append/3, clause No.2' によって、修正案が 「test モジュールにある 3 引数の述語 append の 2 つ目の定義節」 に関する修正案であることがわかります。Priority 1 の2つ目の修正案が意図通り の修正ですが、1つ目の修正案は、2つのリストの要素を交互にマージするプログラ ムになっています(文献[1,3])。 Kima は、修正案の探索に先立って、モード/型制約の矛盾する極小部分集合(以下 では MIS)および、検出規則に違反している(変数)記号を誤りの原因として求めま す。誤りの原因を表示するには、以下のようにします。 % kima +mis append.kl1 < Minimal Inconsistent Subsets of *Mode* constraints > m/<(test:append)/3,1> = IN imposed by rule HV applied to the variable Y in test:append/3, clause No.2 m/<(test:append)/3,1> = OUT imposed by rule BV applied to the variable X in test:append/3, clause No.2 ----- < Minimal Inconsistent Subsets of *Type* constraints > --Constraints are consistent, and there is no MIS-- < Violations of the syntactic rules of Detection Level 2 > singleton(X) in test:append/3, clause No.2 最初にモード制約に関する MIS が表示され、次に型制約に関する MIS が表示され ます。Kima は独立した複数の MIS を一度に求めることができ(文献[5])、それら を `-----' で区切って表示します。この例の場合、モードに関する MIS が1つだ け見つかります。型制約に関しては矛盾は見つかりません。 この例では、MIS は2つの制約式で構成されています。制約式に続く2行が、制約式 が課される原因となった記号を表しています。たとえば、制約式 `m/<(test:append)/3,1> = IN' を課しているのが、 「test:append/3 の 2 つ目の定義節における変数 Y (とモードづけ規則 HV)」 であることがわかります。したがってこの MIS は、「test:append/3 の2つ目の 定義節における変数 X と Y が誤りの原因として疑わしい」ことを表します。 Kima はこの X と Y の節内の出現数を増減させることによって修正案を探索し ます。 また検出規則2により、変数 X の singleton 出現が誤りとして検出されています。 検出規則の違反は以下のように出力されます。 [検出規則1の違反] - ガードで検査している変数がへッドにない: var_not_in_the_head(変数名) - ユニフィケーションの両側に同一の変数が出現している: not_pass_occur_check(変数名) [検出規則2の違反] - 下線 ``_'' で始まっていない singleton 変数がある: singleton(変数名) 例 2: 独立する 2 箇所の誤り 次に、確率統計学における「組合せ」を計算するプログラムにおいて、2箇所の変 数を間違えている例を考えます。 +--------- comb.kl1 ---------------------------------------------+ | :- module probability. | | | | % nCr (n >= r >= 0) | | % Use: combination(N,R,C) | | % e.g. combinaiton(3,2,Res) --> [[1,1,0], [1,0,1], [0,1,1]] | | combination(N,0,C) :- true | init_list(0,N,0,[],C0), C=[C0]. | | combination(N,N,C) :- true | init_list(0,N,1,[],C0), C=[C0]. | | combination(N,R,C) :- N>R | | | N1:=N-1, R1:=R-1, | | combination(N1,R1,C0), cons_list(1,C0,CC0), | | combination(N1,R, C1), cons_list(0,C1,CC1), | | append(CC0,CC1,CC). | | % C <-- correct | | | | init_list(N,Len,_,L0,L) :- N =:= Len | L0=L. | | init_list(N,Len,E,L0,L) :- N < Len | | | L1=[E|L0], N1:=N+1, init_list(N1,Len,E,L1,L). | | | | cons_list(_,[], L) :- true | L=[]. | | cons_list(A,[X|Xs],L) :- true | | | L=[[A|X]|L1], cons_list(A,XS,L1). | | % Xs <-- correct | | | | append([], Y,Z ) :- true | Y=Z. | | append([A|X],Y,Z0) :- true | Z0=[A|Z], append(X,Y,Z). | +----------------------------------------------------------------+ これに対して深さ1の修正案を探索します。 % kima comb.kl1 ================= Suspected Group 1 ================= ------------- Priority 1 ------------- combination(N,R,CC):-N>R|N1:=N-1,R1:=R-1,combination(N1,R1,C0), cons_list(1,C0,CC0),combination(N1,R,C1),cons_list(0,C1,CC1), append(CC0,CC1,CC) in probability:combination/3, clause No.3 ----- ================= Suspected Group 2 ================= ------------- Priority 1 ------------- cons_list(A,[X|XS],L):-true|L=[[A|X]|L1],cons_list(A,XS,L1) in probability:cons_list/3, clause No.2 ----- 2つの Suspected Group があるのがわかります。Kima は、修正案探索に先だって 求めた複数の MIS を、その原因である節が重なっているかどうかを検査すること でグループ化します。深さ N の修正案の探索は、それぞれのグループごとに独立 して行なわれます。この例の場合、Kima は変数の2箇所の誤りが独立するグループ に属すると判断して、それぞれのグループに対して深さ1の探索を行ない、意図通 りの修正案を求めることに成功しています。ここで提示された修正案は、オリジナ ルのプログラムから変数名を変えただけの等価なプログラムであることに注意して ください。誤り箇所のグループ化やプログラムの等価性に関しては、文献[2-4]を 参照してください。 例 3: 同一グループの 2 箇所の誤り クイックソートを行なうプログラムにおいて、同一節中の変数を2箇所書き間違え ている例を考えます。 +--------- qsort.kl1 -------------------------------------------------------+ | :- module main. | | | | main :- true | quicksort([3,8,2,5,6],Res),io:ousstream([print(Res),nl]). | | | | quicksort(Xs,Ys) :- qsort(Xs,Ys,[]). | | qsort([], Ys0,Ys ) :- true | Ys=Ys0. | | qsort([X|Xs],Ys0,Ys3) :- true | | | part(X,Xs,S,L), qsort(S,Ys0,Ys1), | | % Ys1=[X|Ys2], qsort(L,Ys2,Ys3). <-- correct | | Ys2=[X|Ys1], qsort(L,Ys2,Ys3). | | | | part(_,[], S, L ) :- true | S=[], L=[]. | | part(A,[X|Xs],S0,L ) :- A>=X | S0=[X|S], part(A,Xs,S,L). | | part(A,[X|Xs],S, L0) :- A< X | L0=[X|L], part(A,Xs,S,L). | +---------------------------------------------------------------------------+ これに対して深さ1の探索を行なっても、修正案を見つけることはできません。 % kima qsort.kl1 ================= Suspected Group 1 ================= Sorry, no alternative is found そこで、深さ2の探索を試みます。 % kima +d 2 qsort.kl1 ================= Suspected Group 1 ================= ------------- Priority 1 ------------- qsort([X|Xs],Ys0,Ys3):-true|part(X,Xs,S,L),qsort(S,Ys0,Ys1),Ys1=[X|Ys2], qsort(L,Ys2,Ys3) in main:qsort/3, clause No.2 ----- その結果、意図通りの修正案が唯一の修正案として求まります。 このとき、もし深さ1の探索による修正案が存在する場合は、それらを同時に求め、 同じ条件で優先度づけして出力します。つまり、深さ N の探索による修正案は深 さ 1, ..., N-1 の探索による修正案を含みます。 Kima が提示する修正案が意図通りのものであるかどうかは、ユーザが自分で判断 しなければなりません。 4. 詳しい使用法 (コマンドラインオプションについて) Kima では、コマンドラインオプションを指定することで、検出のみの実行やモー ド/型の選択的利用、探索の深さ(変数記号出現の書換え個数)の指定などの細かい 制御を行なうことができます。 以下のコマンドラインオプションが利用可能です。 ----------------------------------------------------------------- オプション 効果 ----------------------------------------------------------------- +mode モード制約の矛盾する極小部分集合だけを利用します。 +type 型制約の矛盾する極小部分集合だけを利用します。 +dr 検出規則 1, 2 (検出レベル2) のみを利用します。 +mis 誤りの原因、すなわち矛盾する極小部分集合および 検出規則に違反している(変数)記号を出力します。 +d N 個までの書換えを行なって修正案を探索します。 ただし N は 0 優先度 N までの修正案を表示します。 ただし N は N>0 を満たす整数です。 +pp ペナルティ値が N より大きな修正案は探索しません。 ただし N は N>0 を満たす整数です。 +h ヘルプを表示します。 ----------------------------------------------------------------- これら以外のコマンドライン引数は、すべてファイル名として処理されます。存在 しないファイル名が指定された場合、Kima は実行を中止します。 オプションが何も指定されなかった場合、Kima はオプションが % kima +mode +type +dr +d 1 +p 1 +pp 20 FILE1 FILE2 ... であるものとみなします。つまり、モード/型制約およびレベル2までの検出規則を 利用し、変数を1箇所書換える修正案の探索を行なって、最も優先度の高い修正案 だけを求めます。 Kima は以下の原則に基づいてコマンドライン引数を解釈します。 - `+mode', `+type', `+dr' のうち、どのオプションも指定されなかった場合、 これら3つのオプションがすべて指定されているとみなします。 - `+mis', `+d' のどちらのオプションも指定されなかった場合、`+d 1' が指定 されているとみなします。極小部分集合と同時に修正案も求めたい場合は、 `+mis +d ' のように指定します。 - `+d', `+p', `+pp' の引数 N のデフォルト値は、それぞれ 1, 1, 20 です。 - オプション `+d', `+p', `+pp' が指定されたにも関わらず、引数 N が与えら れなかった場合、オプションの指定自体を無視します。 - `+h' は必ずオプションの先頭で指定する必要があります。 通常の UNIX コマンドと違い、オプションが `+' 記号で始まっていることに注意 して下さい。KLIC 処理系によって `-' で始まるオプションが使用済みであるため、 このような仕様になっています。 5. インストール Kima は KL1 言語だけで記述されており、KLIC 処理系を使ってコンパイルします。 インストール方法については、本ファイルと同様に配布キットに含まれている INSTALL (INSTALL-j) を参照してください。 また、配布キットは下記のファイル群で構成されています。 (1) Makefile -- make ファイル (2) Readme-j -- 本ファイル Readme -- 本ファイルの英語版 (3) INSTALL-j -- インストールマニュアル INSTALL -- インストールマニュアルの英語版 (4) ChangeLog -- 第2.1版からの変更点の一覧 (5) kima-mainC.kl1 read_program4.kl1 normalize5.kl1 unify.kl1 builtin_DB_st6.kl1 numberbuiltin3.kl1 findpath4.kl1 constraints_stC.kl1 type_st2.kl1 stdinout2.kl1 minsub.kl1 type_minsub.kl1 copygraph3.kl1 tcopygraph.kl1 group_doubt3.kl1 generate_testB.kl1 gen_alt7.kl1 test_altA.kl1 heuristicsB.kl1 common3.kl1 probability3.kl1 command_line5.kl1 normalize_num.kl1 path_utility.kl1 graphH.kl1 decode2.kl1 reduce6.kl1 sort.kl1 outmessage5.kl1 tdecode.kl1 tgraph_st5.kl1 -- Kima のソースプログラム (全 31 ファイル) (6) examples/append-error.kl1 comb-error.kl1 fib-error.kl1 qsort-d2-error.kl1 -- バグ入りプログラムのサンプル(第3節で紹介したものを含む) 6. klint による(型)解析との主な相違点 Kima は、KL1 プログラム静的解析系 klint ver.2 (文献[8])を利用して作成 されていますが、型解析に関しては、異なる点が2つあります。 (1) klint ver.2 は強型体系を前提としていません。Kima では、データ型を以下 のように分類し、同一のパスに異なる関数記号が出現するのを禁止することで、 (単純な)強型体系を定義しています。 型 種類 KLIC 処理系における wrapped term ---------------------------------------------------------------- F1 整数 integer(Int) F2 浮動小数 floating_point(Float) F3 文字列 string(Str) F4 ベクタ vector({Elem, ...}) F5 リスト list([Car|Cdr]) または atom([]) F6 ストラクチャ functor(Functor(Arg, ...)) または atom(Atom) ただし Atom は `[]' 以外 (2) Kima では、リストの cdr がもとのリストと同じ型である: for all paths p, p = p という制約を課します。これは klint では行なわれません。 7. 未実装の機能について (1) プログラムの層化(stratification) (2) 誤りの原因をさらに絞り込む「方針 1, 2」(文献[1,3]) (3) 完全な変数出現検査(occur-check) 特に(1)が未実装であるために、append や length のような多層モード/型を許す 述語をプログラムの複数の場所から呼び出すと、well-moded/typed なプログラム でも、モード/型誤りが発生する可能性があります。これは特に型に関して深刻で す。これを回避するには、同一の述語を呼出しごとに他の名前で複数定義するなど の(アドホックな)措置をとらなければなりません。 8. 制限 (1) ベクタにストリーム(変数)をそのまま格納すると、ill-moded になります。こ れは現在の KLIC 処理系が、new_vector/2 に対して new_vector(Vector,Integer) と new_vector(Vector,List) という2つの使い方を許しているからです。Kima は new_vector がすべて前者のように使われていると仮定してモードづけしますが、 このとき、KLIC 処理系はベクタの要素をすべて 0 で初期化しますので、ベクタの 要素のトップモードはかならず in になります。そのため、out に制約されるスト リーム(変数)をベクタにしまうとモード誤りを引き起こします。これは Kima が利 用している klint においても同様です。 (2) 変数の修正を行なう場合、節における「全く新しい変数」への修正を考慮する 必要がありますが、Kima では、これのために `FreshVarN'(N は 0 から 9 までの 整数値) という変数名を使っています。そのため、もともとのプログラム中でこの `FreshVarN' という変数が使われていると、修正案が正しく提示されない可能性が あります。`FreshVarN' という変数名の利用はできるだけ避けて下さい。 (3) 「リストの cdr はもとのリストと同じ型である(6節(2))」という制約を課し ているため、標準出力やファイル出力へのストリームに任意の型のデータを流すと、 型誤りが発生してしまいます。したがって、Kima を適用する際には、標準出力や ファイル出力への書き込みを行なっている部分をコメントアウトする必要がありま す。 (4) Kima が klint ver.2 を利用している関係上、klint ver.2 における制限が、 そのまま Kima の制限になっています。また、klint でサポートしていない KL1 言語の機能については、Kima でもサポートしていません。klint ver.2 に関して は、文献[8]の Readme 等を参照してください。 参考文献 [1] Ajiro, Y., Ueda, K., Cho, K., Error-Correcting Source Code. In Proc. Fourth Int. Conf. on Principles and Practice of Constraint Programming (CP'98), LNCS 1520, Springer, 1998, pp.40-54. [2] Ajiro, Y., Ueda, K., Kima: an Automated Error Correction System for Concurrent Logic Programs. Automated Software Engineering, Vol.9, No.1, Kluwer Academic Publishers, January 2002, pp.67-94. [3] Ajiro, Y., Automated Programming Framework Using Constraint-Based Static Analysis, Ph.D. Thesis, Waseda University, March 2002. [4] 網代育大, 上田和紀: Kima: 並行論理プログラム自動修正系. コンピュータ ソフトウェア, ソフトウェア発展特集, Vol.18, No.0, 2000, pp.122-137. [5] Cho, K. and Ueda, K., Diagnosing Non-Well-Moded Concurrent Logic Programs, In Proc. 1996 Joint Int. Conf. and Symp. on Logic Programming (JICSLP'96), The MIT Press, 1996, pp.215-229. [6] Ueda, K. and Morita, M., Moded Flat GHC and Its Message-Oriented Implementation Technique. New Generation Computing, Vol.13, No.1 (1994), pp.3-43. [7] Ueda, K., Experiences with Strong Moding in Concurrent Logic/Constraint Programming. In Proc. Int. Workshop on Parallel Symbolic Languages and Systems, LNCS 1068, Springer, 1996, pp.134-153. [8] Ueda, K., klint - Static Analyzer for KL1 Programs. Available from http://www.ueda.info.waseda.ac.jp/software.html, 2000.