A semantic editor

摘要

We describe an interactive tool for program development and transformation, a semantic editor. The domain of the semantic editor is Backus's FP programming language. The editor facilitates manipulation of FP program schemas by the meaning-preserving transformations of FP's algebra of programs. The semantic editor aids program development, program optimization and equivalence proofs. It also serves as a tool for investigating the algebra of programs itself.

rn

The semantic editor does not depend on the existence of normal forms for FP programs. Instead, a history of all program transformations is retained in the system in the form of a congruence relation. The user is free to step through the congruence classes to see different but equivalent versions of his programs. A program equivalence is applied to a program schema by unifying one side of the equivalence with a sub-program, then labeling it congruent to the other side if the unification is successful. A congruence closure algorithm is applied to find any new congruence relations in expressions containing these program schemas.

rn

The program schemas are represented internally by a directed, acyclic graph (dag) with identical sub-programs occupying the same sub-graph. The semantic editor uses the Patterson and Wegman unification algorithm and the Nelson and Oppen congruence closure algorithm. Both employ the dag representation. The system is implemented in Scheme, a dialect of Lisp.