Skip to main content

Section 6.7 Summary and Further Reading

In this section, we discussed a formal semantics of a very small subset of C called C0. We used a small-step operational semantics for formalizing C0's statements. There are other approaches of formalizing semantics as well but small step semantics are very close to the intuitive understanding of program execution. We have particularly paid attention to modelling all different program behaviors (terminating, aborting, diverging, getting stuck). We will come back to this when discussing formal verification later on.

C0 leaves out, by choice, many aspects of C which make formalizing C more involved, such as a realistic memory model, side effects in expressions, and so on. All these details are covered by more comprehensive formalizations of C in the dissertations of Norrish [8] and Krebbers [9] and in the verified C compiler CompCert [10].

Very good introductions to formal semantics of programming languages are the textbooks by Nielson and Nielson [5] and Winskel [7]. More advanced topics are covered in the book by Harper [6] and, with more focus on type systems, by Pierce [11].