This paper describes a methodology for defining an executable abstract interpreter from a formal description of the semantics of a programming language. Our approach is based on Skeletal Semantics and an abstract interpretation of its semantic meta-language. The correctness of the derived abstract interpretation can be established by compositionality provided that correctness properties of the core language-specific constructs are established. We illustrate the genericness of our method by defining a Value Analysis for a small imperative language based on its skeletal semantics.

翻译：本文提出一种从编程语言的形式化语义描述中定义可执行抽象解释器的方法论。我们的方法基于骨架语义及其元语言的抽象解释。只要建立核心语言特定构造的正确性属性，即可通过组合性证明所推导抽象解释的正确性。我们通过基于某小型命令式语言的骨架语义定义其值分析，说明本方法的通用性。