A Formal Compiler Specification Method

The paper presents a new formal compiler specification method that has evolved out of a number of realistic applications. The method is characterized by a predicate calculus formalism with an interpretation domain consisting of a structured pair of source and target derivation (parse) trees. The translation mechanism progresses via a monotonic growth of the target derivation tree upon selected application of a finite set of rules based on the predicate calculus of the formalism . The novelty of the method lies in its power to treat contextual dependency of the target code on remotely distributed parts of the source code. In alternative words the method handles nontrivial translation situations where dependencies between source and target codes cannot be reduced to local-to-local correspondences. The method was succesfully applied to design and to implement an SDL-to-S/R compiler, where the former is an ITU-T standard language popular in telecommunication software world and the latter i..