Nov. 12, 1995 to Nov. 15, 1995
J. Richardson , Dept. of Artificial Intelligence, Edinburgh Univ., UK
I present an automatic technique for transforming a program by changing the data types in that program to ones which are more appropriate for the task. Programs are synthesised by proving modified synthesis theorems in the proofs-as-programs paradigm. The transformation can be verified in the logic of type theory. Transformations are motivated by the presence of subexpressions in the synthesised program. A library of data type changes is maintained, indexed by the motivating subexpressions. These transformations are extended from the motivating expressions to cover as much of the program as possible. I describe the general pattern of the revised synthesis proof, and show how such a proof can be guided by difference matching followed by rippling.
data structures; functional programming; theorem proving; program verification; type theory; programming theory; software libraries; libraries; automatic technique; automated data type changes; functional programs; program transformation; program synthesis; modified synthesis theorem proving; proofs-as-programs paradigm; type theory logic; verification; subexpressions; data type change library; revised synthesis proof; difference matching; rippling
J. Richardson, "Automating changes of data type in functional programs", KBSE, 1995, Knowledge-Based Software Engineering Conference, Knowledge-Based Software Engineering Conference 1995, pp. 166, doi:10.1109/KBSE.1995.490132