Models and Interpretations: Formalizing Multiple Semantics
Abstract
We often think of a program as having different meanings in different contexts. When inferring types, for example, a compiler computes an upper bound on the possible types of each expression during execution. These upper bounds can be thought of as an interpretation of the program. When writing numerical software a programmer sometimes reasons as if the program operated on mathematical real numbers but at other times reasons about numbers with only finite precision, two rather different interpretations. This paper defines formal notions of interpretation and model to provide a counterpart to our intuitive understanding of the meanings of a program. Briefly, an interpretation is an assignment of labels to program terms, subject to constraints imposed by a model. This formalization lets us reason rigorously about relationships between different meanings and provides a conceptual framework for designing algorithms for program analysis, transformation, and execution. We develop and motivate the details through the example of a model in which an interpretation is a program's (interprocedural) flow graph. We also briefly discuss several other models in which interpretations are computed as part of the transformation and compilation machinery of the E-L programming environment and language.
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 01, 1989
- Accession Number
- ADA276413
Entities
People
- Michael Karr
- Steve Rosen