Formal Methods during the Programming Phase

Formal methods involves the application of sound mathematical specification and reasoning techniques to the development of software systems. They can be applied across all phases of the engineering lifecycle. This chapter discusses their specific application to the programming phase, which can entail enrichment of executable code with mathematical artefacts (to support and improve our capabilities for reasoning), and the derivation of executable code from mathematical specifications. We provide an overview of some of the important approaches that can be applied to this phase.