Analogical program derivation based on type theory

AbstractOur goal is to develop a formal method for analogically deriving programs from past programming experience. It is commonly recognized that program development plays a central role in analogical programming. This paper proposes to use a calculus to uniformly represent specification, program, and the development from the former to the latter. Thus analogical reasoning can be discussed in a single framework. In this framework, we first propose an analogy matching method to seek the analogical correspondence between two specifications based on a generalization procedure. Secondly, the analogical correspondence is used as a basis for transforming existing program derivations to new ones. The corresponding program can be obtained by simple calculation of its type. Finally, an example is given to illustrate our method