Hierarchical semantics, reasoning, and translation
Jonathan C. Shultis · 1982
A framework is presented for the formal specification, analysis, and translation of programming languages. The framework is built around SSL, an algebraic metalanguage capable of expressing and manipulating semantics on many levels of abstraction. SSL supports a general method for determining the static properties of languages and their programs by computing with homomorphic images of their definitions. The use of SSL to define a programming language and derive algebraic proof rules for reasoning about the defined language is demonstrated. Translation of programs written in languages that are defined in SSL is effected by transforming the programs's SSL semantics from a source-level dialect of SSL to a target-level dialect. The transformations are proved correct using the algebraic laws associated with SSL, and the applicability of transformations to particular programs is ascertained by use of the algebraic static analysis technique. Translations can be cascaded through a hierarchy of intermediate languages, each defined in SSL using the abstractions provided by lower levels of the hierarchy. Code improvement by transformation can be effected at each intermediate level.