Analyzing Action Semantics

Kasper Svendsen

AbstractProgrammers usually assume that when they compile a program, the behavior of the generated code corresponds to the semantics assigned to the program by the programming language. However, writing a correct compiler, that generates reasonably efficient code, is a difficult and expensive task. A lot of research has therefore focussed on automatically generating complete compilers from formal specifications of languages. In some cases, even with an accompanying proof of correctness of the generated compiler.

In this thesis we develop a tool for analyzing semantic descriptions of programming langauges, specified in a subset of the semantic description language, Action Semantics. The purpose of the tool is to function as a component of a compiler generator.

The tool implements two analyses: The first analysis is a type and termination analysis, which annotates semantic descriptions with type information about the values, that programs written in the described language can produce. The second analysis analyzes the use of bindings in the languages specification, to generate a bindings analysis for the source language.
TypeBachelor of Engineering thesis [Academic thesis]
Year2007
PublisherInformatics and Mathematical Modelling, Technical University of Denmark, DTU
AddressRichard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby
SeriesIMM-B.Sc-2007-13
Electronic version(s)[pdf]
BibTeX data [bibtex]
IMM Group(s)Computer Science & Engineering