(16)Static Analyzer of KL1 Programs

********************************************************************
                klint - Static Analyzer for KL1 Programs
                                                                    
                              Version 2.1
                              January 1999
                                                                    
                             Kazunori Ueda
             Department of Information and Computer Science
                           Waseda University
                      ueda@ueda.info.waseda.ac.jp
                   Copyright (C) 1999  Kazunori Ueda
                                                                    
                               -- and --

      Kima -- an Automated Error-Correction System of KL1 Programs

                              Version 2.0
                              January 1999

                   Yasuhiro Ajiro, Kazunori Ueda                    
             Department of Information and Computer Science
                           Waseda University
                  {ajiro,ueda}@ueda.info.waseda.ac.jp
           Copyright (C) 1999  Yasuhiro Ajiro, Kazunori Ueda
********************************************************************


1. OVERVIEW

1.1  Klint version 2.1

Klint v2.1 is a constraint-based static analyzer of KL1 programs, which
performs 

  - mode analysis, 
  - linearity analysis, and
  - type analysis.

The key feature of klint v2.1 is mode analysis.  It analyzes the mode
of a KL1 program using the ideas described in [1].  Well-modedness
roughly means that the communication protocols used in a program are
cooperative.  It is highly recommended to write your KL1 programs in a
well-moded manner, because it enables the klint system to detect many
of program errors statically [3].

Klint v2.1 also analyzes the linearity and the type of the program.
Linearity analysis distinguishes data that are guaranteed to be
referenced from only one reader occurrence of a variable from data
possibly shared by two or more occurrences of variables [6].
Linearity analysis provides basic information for compile-time garbage
collection.

Types in klint v2.1 express what categories of function symbols may
occur at each path (= position in a data structure that a goal may
possibly have as its argument).

Klint v2.1 does not require programmers to provide mode, linearity, or
type declarations; instead, klint v2.1 will infer the
mode/linearity/type of a given program.  An introductory article of mode
analysis can be found in [2].


1.2  Kima version 2

Kima ver.2 can correct near-misses of KL1 programs automatically by mode
and type analysis [5].  Near-misses are a few wrong variable symbol
occurrences in KL1 programs.  Most of simple errors occur on variable
symbols because variable symbols are used heavily in (concurrent)
logic/constraint programs, and it is not easy for programmers to correct
such misses.  So Kima's function is very reasonable and useful.  Even
when Kima ver.2 fails to correct errors, it can identify a small number
of suspected symbols that cause mode and type errors [4].


2. INSTALLATION

Klint v2.1 and Kima v2 are totally written in KL1 and can be compiled
using KLIC running under a UNIX system.

The klint v2.1 distribution contains the following files:

  (1) Makefile -- make file
  (2) Readme-E -- This file
      Readme-J -- Japanese version of this file
  (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
	       -- source files of klint v2.1
  (4) examples/merge.kl1, examples/hamm.kl1
               -- sample KL1 programs used in this manual
  (5) kima-v2/ -- directory of the kima v2, a diagnoser for KL1
                  programs.  See kima-v2/Readme and kima-v2/INSTALL for
                  more details.


REFERENCES

[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] Ueda, K.,  Linearity Analysis of Concurrent Logic Programs.  IPSJ
SIGPRO meeting, August 1998.  (in Japanese)

[FTP]

• README
• Program and Documents [99K]