ABSTRACT
In this chapter, we resume discussion of the idea of correctness by construction that was introduced in Section 7.4. In particular, we look at the actual implementation of source code with an emphasis on one particular technique, the SPARK approach. We begin by looking at what goes wrong in implementing software so that we can see the scope of the problem and how correctness by construction can help.
