Formal semantics and C (completed)

When we want to know how a programming language construct such as Java exception handling works, we look it up in the language manual or a textbook. This is good enough for most programmers since they can test their understanding by compiling short programs and watching their effects in a debugger. However, compiler developers have to be sure that their compiler works correctly in all possible cases and they do not usually have a ‘gold standard’ implementation against which to test their understanding.

Language manuals and text books use normal human languages to describe how a program should behave, and of course human language is often imprecise (and descriptions may be incomplete). Formal semantics is that branch of Computer Science which attempts to specify the meaning of programming language constructs using unambiguous, complete and precise specifications. In practice this means using aspects of mathematics, in particular logical inference, to describe program behaviour.

Writing a traditional formal semantics for a large language is hard, and as a result language designers and compiler writers rarely use formal techniques when developing real languages. However, the FunCon approach developed by the PLanCompS project at Swansea and Royal Holloway offers an approachable alternative: the technique embeds the mathematical detail in a modular, extensible notation that abstracts away the most difficult aspects of formal semantics. We have successfully used the new approach with undergraduates in our final year Software Language Engineering course (CS3480) to specify and execute toy languages.

We want to use this new FunCon approach in the development of a formal semantics for ANSI-standard C. We have chosen this language because (a) the language is ubiquitous, (b) there is a well defined suite of test programs supplied with the Open Source GNU C compiler, and (c) one of our collaborator research groups in the US has developed a formal semantics for ANSI-C using their own formal semantics techniques, and it would be interesting to compare our approach to theirs.

Since this is research, we do not know how much we can realistically achieve in the time available, and a student taking on this project would in any case have to learn many new techniques. As a result, the project is rather open ended and we might extend it in the future. You would be working with Adrian Johnstone, Elizabeth Scott and Thomas van Binsbergen who is actively developing interpreters for the FunCon system as part of his PhD project.

You will need to be proficient in Java and to have a strong interest in the design and implementation of programming languages. The project will develop skills that can support your undergraduate achievements: in particular this project would provide an excellent introduction to some of the material in CS3470 Compiler Theory and CS3480 Software Language Engineering, and there is also scope for designing final year projects that build on this work.