Aspect of the interaction between compiler theory and practice is addressed. Presented is a technique for the syntax-directed specification of compilers together with a method for proving the correctness of their parse-driven implementations. The subject matter is presented in an order-algebraic framework; while not strictly necessary, this approach imposes beneficial structure and modularity on the resulting specifications and implementation correctness proofs. Compilers are specified using an order-algebraic definition of attribute grammars. A practical class of compiler implementations is considered, consisting of those driven by LR( k ) or LL( k ) parsers which cause a sequence of translation routine activations to modify a suitably initialized collection of data structures (called a translation environment). The implementation correctness criterion consists of appropriately comparing, for each source program, the corresponding object program (contained in the final translation environment) produced by the compiler implementation to the object program dictated by the compiler specification. Provided that suitable intermediate assertions (called translation invariants ) are supplied, the program consisting of the (parse-induced) sequence of translation routine activations can be proven partially correct via standard inductive assertion methods.

This paper presents a formulation, within the framework of initial algebra semantics, of Knuthian semantic systems (K-systems) which contain both synthesized and inherited attributes. This formulation permits a precise definition of K-systems, and combines their intuitive appeal with the theoretical power of algebraic methods. The basic approach consists of algebraically specifying the semantic portion of a given K-system, converting this K-system into another equivalent one which contains only synthesized attributes, and then defining the new equivalent K-system by means of an algebraic formulation. The practical implications of the algebraic definition of K-systems are discussed, and the combined use of Knuth's original formulation and the algebraic approach for the development of semantic definitions is advocated.