Sort Inference in Action Semantics

[摘要] Action semantics is a semantic meta-language developed by Mosses and Watt for specifying programming languages. The work reported in this thesis is part of a project to develop a system, called ACTRESS, that is a semantics-directed compiler generator based on action semantics. The aims of this project are to demonstrate the suitability of action semantics for this task, and to produce a system that improves on the performance of previous semantics-directed compiler generators. Moreover the ACTRESS system aims to accept a wide range of programming languages, including dynamically-scoped and dynamically-typed languages, but not to penalise the implementations of statically-typed or statically-bound languages as a result. ACTRESS automatically generates a compiler from an action semantic description of a programming language, and has been used to generate compilers for a small declarative language and a small imperative language. The generated compiler uses a number of standard modules to compile the action denoting a program into efficient object code. Amongst these modules is the action notation sort checker. The role of the action notation sort checker is vital. It analyses an action and infers detailed information about the sorts of data flowing between the sub-actions. Without this information, erroneous actions could not be detected, and efficient code generation would not be possible. The problem of sort inference for action notation is a complicated one. Firstly, action notation has an unusual sort system, which includes individuals as sorts, sort join, and sort meet. Secondly, the complex data flows in action notation prevent a simple bottom-up or top-down analysis. In general, actions have polymorphic sorts. Thirdly, we aim to be as general as possible, and allow actions that still require sort checks when the action is performed. We must detect the places in an action where a run-time sort check is necessary, and annotate the action accordingly. In this thesis, we present a sort inference algorithm for action notation, that is specified as a collection of sort inference rules, and we describe the implementation of this algorithm to produce the action notation sort checker. Furthermore, we formulate a soundness property for our sort inference algorithm, and prove its soundness with respect to the natural semantics of ACTRESS action notation. Finally, we compare ACTRESS with other semantics-directed compiler generators that use action semantics, and suggest possible improvements and future research.

[发布机构] University:University of Glasgow

[关键词] Computer science