KL1 is a concurrent logic programming language born in the Fifth Generation Computer Systems (FGCS) project promoted by the Ministry of Internationl Trade and Industry, Japan. KL1 was designed for symbol processing on parallel computers, and heavily used as a kernel language in that project. KL1 is one of (logic) programming languages that achived the most satisfactory results.
A concurrent logic language is a language such that
In execution of a concurrent logic program,
Concurrent logic languages are a kind of high level languages, and its efficiency is inferior to that of programs written properly in low level languages such as C. However, the research is now in progress to improve the efficiency of concurrent logic programs with the assistance of static analysis.
A KL1 compiler, KLIC, translates KL1 program to C program and makes it executable using gcc. KLIC can be installed on most of UNIX like workstations and PCs. KLIC is available from KLIC site. You can enjoy parallel programming on multi-processer servers produced by Sun Microsystems Inc. or multi-processor PC/AT compatible computers.
(Concurrent) logic languages are amenable to static analysis that reasons the property of programs, because logic languages are based on first-order predicate logic and are theoretically tractable. A static analysis of Moded Flat GHC programs is under investigation in our group. The static analysis system is built additionally into Flat GHC, which is a subset of GHC (Guarded Horn Clauses) KL1 is based on. KL1 is a programming language in which several constructs, syntax sugar, and built-in predicates are added into Flat GHC.
Objective of static analysis is, for example, to verify:
The main difference between concurrent/distributed computing and sequential computing is that there is communication in the midst of sequential computation. Real-time computing can also be formalized as sequential computation accompanied with communication with the outer world. This simple, but important, differnce makes the behavior of programs surprisingly complicated, difficult to understand, and therefore difficult to debug. Static analysis is thus indispensable to manifest the complicated behavior which is quite invisible in communicative environment. Moded Flat GHC is an eligible computation model as well as a programming language for concurrent/distributed computing.
K ima
The first version of Kima was written by Kenta Cho in our research group. Kima was named after the Analyzer of Ill-Moded KL1 programs. The first version is available from ``KL1 Programming Support System'' in AITEC Contract Research Projects in FY1996. Kima v1 locates multiple bugs in small regions of program text when KL1 program includes bugs. This is done by assuming strong moding and typing of Moded Flat GHC onto KL1 programs. KL1 is designed based on Flat GHC,and strong moding and typing of Moded Flat GHC are also applicable to KL1. The application turned out to benefit the debugging of KL1 programs from our experiences.
Kima version 2 we developed by extending the v1 corrects bugs automatically as far as the bugs are near-misses, that is, errors on the occurrences of variable symbols. Please refer to papers or README included in the archive. Kima v2 is based on klint version 2.1 - Static Analyzer of KL1 Programs.
Kima runs on most of Unix like OS.