A knowledge-based approach to loop analysis is presented. First-order predicate logic annotations are generated as a result of the analysis. A taxonomy classifies loops according to their complexity. Dataflow analysis is used to decompose loops into closely related statements that are encapsulated into events. Patterns, called “plans,” from a knowledge base are used to extract loop specifications. Specifications of individual events are synthesized into a consistent, rigorous functional abstraction of the whole loop. The authors performed a case study of an existing, reasonable-sized program to test the process and its effectiveness.

Loop conditions are converted into conjunctive normal form (CNF) to achieve representation independent of a programming language and specific implementation details. The taxonomy for classifying loops includes three dimensions: control computation, complexity of condition, and complexity of body. At present, the approach does not include loops with recursive calls. A complete discussion of the analysis of flat loops is given before the analysis of nested loops is developed. The nested loop process includes a context adaptation phase and the introduction of a formalism called an abstraction class.

As might be expected, the authors note that the tasks of designing plans and managing the knowledge base require expertise in both the application domain and formal specifications. The program for the case study involves scheduling a set of university courses. It has 1400 lines of Pascal source code, with 39 subprograms and 77 loops from all classes in the taxonomy. The authors note that “as the number of analyzed loops increased, the experience gained led to the evolution of the knowledge base. The monitored usage of the knowledge base served to improve some of the plans in terms of their structure, knowledge representation, number, and naming conventions. As a result, the knowledge base was more suitable for the domain under consideration.”

LISP-based LANTeRN, which stands for “loop analysis tool for recognizing natural concepts,” is the prototype tool developed by the authors to demonstrate the feasibility of automating their knowledge-based analysis approach. LANTeRN’s output includes loop classification, loop events and matching plans, individual event analysis results, and final results.

This paper describes an effective way to partially automate the formal analysis of loops via a knowledge base. I recommend it to all professionals interested in analysis of control structures, application of knowledge engineering to language constructs, or automation of formal specifications.