Structuring transformational developments: A case study based on Earley's recognizer (Q792748)

''Transformational programming'' characterizes a methodological approach to the (formal) development of correct algorithms from (descriptive) problem specifications by means of step-wise, (usually) user-guided application of correctness-preserving transformation rules. Although this approach prospered well in the last decade, and may be considered an established discipline in the field of programming methodology today, there are still a number of open problems. One of them concerns the exploration of principles in transformational developments and the development of appropriate notations for expressing these underlying principles in a transparent way, e.g. in order to make them suited for (human) communication. The paper was intended to contribute to solving this particular problem by presenting, as a substantial case-study, a complete transformational development of a non-trivial algorithm for recognizing context-free grammars, known as ''Earley's recognizer''. The entire development leads from the descriptive specification of the problem, as it is known from formal language theory, to an efficient procedural program, as it can be found in standard text-books on compiler construction. The underlying principles in this development are made visible by structuring the development into three, hierarchically ordered, conceptual levels: The top level indicates the major goals to be achieved, viz. - derivation of a recursive solution from the initial specification - improvement of the recursive solution (with respect to the next step) - transition to efficient procedural programs. The second level breaks each of these goals into a sequence of more refined subgoals, characterizes them, and gives the sequence of elementary transformations that allows to achieve the respective subgoals. The third level then deals with technical questions, e.g. with the formal verification of the applicability conditions of the elementary transformation rules, or the decomposition of a rule into a combination of more elementary ones. The paper is to be seen as a first attempt to solve the problem of expressing transformational developments in a more conceptual way while still giving enough detailed technical information to allow the validation of the development by an interested reader. Although there are certain aspects that will need improvement in order to come closer to a satisfactory solution to the above-stated problem, the paper may be considered as a basis for further research in this area.