An Introduction to Imperative Programming

In this section we give a formal account of a very small subset of C, called C0. We will use mathematics to give precise and unambiguous definitions of what a C0 program is and what it means to execute it. This allows us to precisely define the outcome and effects of a program execution. Essentially, we will develop a framework that allows us to execute (interpret) C0 programs in mathematics. Such a formal description is much more precise than any textual rendition. This formal account will shed more light on notions like pointers, addresses, L- and R-evaluation that we have introduced in the previous section in an informal way. To keep the complexity low, we will only consider a very small subset of C and omit a large part of the “syntactic sugar”.

We start with a most basic subset called C0 that only contains a single data type (int), expressions, and a few statements; no types, no functions, no pointers, only global variables.

We first extend C0 to C0p by adding pointers. Thereby, we will formally define the semantics of the pointer operators & and * and clarify the pointer mechanics we have covered informally in the previous section.

Then we will add blocks and their nesting in C0pb. This sheds light on how new containers are allocated, how “dangling pointers” come to be, and how local variables can be hidden by other local variables.

Finally, we will introduce a small type system and see how static typing can be used to identify faulty programs statically, i.e. before they crash.