(3) KL1 Programming Support System

Strong moding and constraint-based mode analysis are expected to play fundamental roles in debugging concurrent logic/constraint programs as well as in establishing the consistency of communication protocols and in optimization. Mode analysis of Moded Flat GHC, a subclass of KL1 to which most KL1 programs belong, is a constraint satisfaction problem with many simple mode constraints, and can be solved efficiently by unification over feature graphs. In practice, however, it is important to be able to analyze non-well-moded programs (programs whose mode constraints are inconsistent) and present plausible "reasons" of inconsistency to the programmers in the absence of mode declarations. The "kima" system we have developed is a static debugging tool for non-well-moded KL1 programs. The basic idea is to find a minimal inconsistent subset from an inconsistent set of mode constraints and indicate the symbol(occurrence)s in the program text that imposed those constraints. When there is redundancy in the whole set of mode constraints, a bug can be pinpointed better by considering constraints not in the minimal subset. The system is able to report multiple, independent bugs at once. For large programs, kima narrows search space by stratifying predicates and tries to produce more intuitive explanations. Stratification plays a fundamental role in introducing mode polymorphism as well.