As part of this course we will be providing you with enough knowledge to realise a non-trivial imperative programming language. We will call this imperative language “Olaf”, for very valid ‘technical’ reasons12, and this section will describe the language by example.
The course itself, however, will not describe how to implement all of Olaf. We do not have the time for that!
Instead, we will concentrate on a smaller ‘core’ representation called “Ola”, and you will be expected to complete the implementation of Olaf in your own time once SPLV is over.
Olaf’s concrete syntax has taken inspiration from main stream imperative languages such as Rust, Java, and C.
Walk-through provides a brief tour of Olaf and its syntax;
Ola provides a briefer overview of Ola and its design;
The remaining sections provide the formal specification for Olaf.
- Abstract Syntax
- Static Semantics i.e. typing rules
- Dynamic Semantics i.e. operational semantics
Although you will have been shown formal typing rules written in LaTeX, writing such rules can be tedious. Instead we will an informal, yet formal, textual notation to describe the specification.