Using many-sorted natural semantics to specify and generate semantic analysis

摘要

We present an extension of natural semantics which can be used to describe the static semantics of imperative and object-oriented programming languages. Furthermore we show that the semantic analysis can be generated from these descriptions. As a side-effect, we get a precise definition of which properties of a programming language are statically decidable and which properties can only be checked dynamically during run-time. As an example, we show how a subset of the Java programming language incorporating the full notion of inheritance can be specified within our mechanism.