(16)KL1プログラム静的解析系に関する研究

********************************************************************
             klint - KL1 プログラム静的解析系 (Version 2.1)
                                                                    
                               上田  和紀
                       早稲田大学理工学部情報学科
                      ueda@ueda.info.waseda.ac.jp
                   Copyright (C) 1999  Kazunori Ueda

                              − および −

            Kima  -- KL1 プログラム自動修正系 (version 2.0)

                           網代育大, 上田和紀
                      早稲田大学大学院理工学研究科
                       早稲田大学理工学部情報学科
                  {ajiro,ueda}@ueda.info.waseda.ac.jp
           Copyright (C) 1999  Yasuhiro Ajiro, Kazunori Ueda
********************************************************************

1. 概要

1.1  klint 第2.1版

klint 第2.1版は、KL1 プログラムのための制約ベースの静的解析系であり、以
下の機能をもっています。

  - モード解析
  - データ参照数解析 (linearity analysis)
  - 型解析

klint 第2.1版の中心的な機能はモード解析で、文献 [1] に述べてある方法で
KL1プログラムのモードを解析します。プログラムが「良くモードづけられてい
る (well-moded)」とは、大まかに言えば、プログラムの中で使っている通信プ
ロトコルが協調的であるということです。KL1 プログラムを well-moded に書く
ことによって、プログラムの誤りをモード解析によって静的に検出できるように
なります [3]。

klint 第2.1版は、プログラム中で扱うデータの参照数と型の解析も行ないます。
データ参照数解析の目的は、一つの変数出現からしか参照されないデータと、複
数の変数出現から参照される可能性のあるデータとを区別することです [6]。こ
のように、参照数解析はコンパイル時ゴミ集めのための基本的な情報を提供して
くれます。

klint 第2.1版における型解析の目的は、どのような関数記号がプログラムの各
パス (ゴールの引数として出現しうるデータ構造の中の個々の場所) に出現しう
るかを調べることです。klint 第2.1版では、関数記号を８つのカテゴリに分類
して解析します。

klint 第2.1版を使うにあたって、プログラマがモードや参照数や型の宣言を与
える必要はありません。それらは klint 第2.1版が推論してくれます。モード解
析の入門的な文献としては[2]があります。


1.2  kima 第2版

Kima ver.2 は、モード解析および型解析を用いて、KL1 プログラム中の変数の
少数個の書き誤りを自動的に修正することができます [5]。KL1 などの(並行)論
理型言語ではプログラム中に変数を多用するため、簡単な誤りの多くはこの変数
の使い方の間違いによって発生します。Kima ver.2 は、多く発生するこのよう
な誤りを静的に修正する能力をもっています。単なる上記のような誤りでない場
合でも、Kima ver.2 は誤りの原因となっている記号の候補を少数個に絞り込ん
で呈示します [4]。


2. インストールおよびファイル構成

klint 第2.1版および kima 第2版は KL1 言語だけで書かれていて、KLIC 処理系
の動くUNIX環境で利用することができます。

klint 第2.1版の配布キットは、下記のファイルからなっています。

  (1) Makefile -- make ファイル
  (2) Readme-J -- このファイル
      Readme-E -- このファイルの英語版
  (3) klint-main4.kl1, read_program4.kl1, normalize5.kl1, unify.kl1
      builtin_DB6.kl1, numberbuiltin3.kl1, findpath4.kl1
      constraintsB.kl1, type.kl1, stdinout.kl1 commandline.kl1
      klint25.kl1, graphF.kl1, tgraph3.kl1, decode2.kl1, tdecode.kl1
      reduce6.kl1, sort.kl1, outgraph.kl1, outdecl.kl1, tc.kl1,
      outconstraints.kl1
	       -- klint 第2.1版のソースプログラム
  (4) examples/merge.kl1, examples/hamm.kl1
               -- このマニュアルで用いた例題プログラム
  (5) kima-v2/ -- kima 第2版のディレクトリ（詳細についてはディレクト
                  リの下の Readme-j, INSTALL-j をお読み下さい）

参考文献

[1] 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.

[2] Ueda, K., I/O Mode Analysis in Concurrent Logic Programming.  In
Theory and Practice of Parallel Programming, LNCS 907, Springer, 1995,
pp.356-368.

[3] Ueda, K., Experiences with Strong Moding in Concurrent
Logic/Constraint Programming.  In Proc. Int. Workshop on Parallel
Symbolic Languages and Systems (PSLS'95), T. Ito, R.H. Halstead, Jr., and
C. Queinnec (eds.), LNCS 1068, Springer, 1996, pp.134-153.

[4] Cho, K. and Ueda, K., Diagnosing Non-Well-Moded Concurrent Logic
Programs.  To be presented at 1996 Joint International Conference and
Symposium on Logic Programming (JICSLP'96), Bonn, Germany, September
1996.

[5] Ajiro, Y., Ueda, K. and Cho, K., Error-correcting Source Code.  In
Proc. Fourth Int. Conf. on Principles and Practice of Constraint
Programming (CP'98), LNCS 1520, Springer-Verlag, Berlin, 1998, pp.40-54.

[6] 上田和紀：並行論理プログラムの参照数解析．情報処理学会プログラミング
研究会，1998年8月．改訂版を「KL1プログラム静的解析系」成果報告書，日本情
報処理開発協会，1999 に所収．

［ＦＴＰ］

• README
• ソースプログラム、マニュアル [99K]