An approach to compiler correctness using interpretation between theories (semantics, data type, verification)
B. H. Levy · 1986
An approach to compiler correctness verification is proposed and research that investigates the mathematical framework and applicability of the approach is presented. This approach is based on interpretation between theories, a concept developed in mathematical logic which provides a basis for proving that one logical theory is correctly mapped into another logical theory. To utilize this concept for the compiler application, it is proposed that the theories include higher-order operators (operators that accept operators as arguments and/or return operators as results) and domain equations. Interpretation between theories has previously been defined for predicate calculus and DLP (an extension of dynamic logic). An extension to predicate calculus is proposed which incorporates Scott's theory of domains. It allows higher-order operators and recursive objects, and can be used to specify the denotational semantics of a programming language. An interpretation between our extended theories and criteria the interpretation must meet to be correct are defined. In the course of developing the definitions, we prove various theorems that show the criteria are sufficient. The interpretation between theories can be used as a formal specification of a computer design. A mathematical proof that the interpretation is correct constitutes a verification that the compiler design is correct. The novel concepts presented by this approach are: (1) Interpretation between theories is defined for theories that allow higher-order operators and domain equations; (2) A compiler design is defined as an interpretation between theories. Preliminary research indicates that this approach has strong intuitive appeal because it models the informal design process, results in concise specifications, and organizes the correctness proof into highly modularized, manageable pieces.