EXPLANATION-BASED LEARNING AND REFORMATION FOR PROGRAM GENERATION,TRANSFORMATION,AND VERIFICATION

点击翻译按钮获取中文摘要

This research aims at developing foundations and applications of explanation-based learning (EBL) techniques for the domain of program generation, transformation, and verification, which is one of the most active area of research field in software science. The results of the research are divided into five parts, each corresponding to a single chapter of the final report. The first two results provide the theoretical foundation of the research, while the other three present the results concerning verification, generation, and transformation, respectively. The are summarizad as follows :1.Meta-facility for a class of equational languages has been developed. This ensures that EBL mechanisms can be incorporated in the reflective framework of the languages.2.Modularity in the framework of equational languages has been studied. In paticular, the modularity of simple termination, which plays an important role in verification and generation, has been formally proved.3.The EBL has been applied to the verification of termination of term rewriting systems. The technique has successfully improved the efficiency of the overall system.4.The EBL has been applied to the program generation based on Kunth-Bendix completion of term rewriting systems. The technique has allowed us to develop an efficient procedure for completion with multiple reduction orderings.5.A program tarnsformation technique which preserves termination has been studied and applied to the analysis of composable combination of term rewriting systems. The EBL is related to the process of generalizing known techniques of tranformation.