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].
