CHAPTER 9 Software Fault Avoidance in Implementation
Learning objectives of this chapter are to understand:
• How faults can be avoided in software implementation using correctness by construction.
• The role of programming languages in software implementation.
• The difficulties that arise with languages like C.
• The advantages of languages designed for dependability such as Ada.
• The role of programming standards.
• The SPARK approach to correctness by construction using low-level specification and mechanical verification.
• How formal verification can be applied easily by practicing engineers.
9.1 Implementing Software
Once we have a specification of what software is to do, we have to develop an implementation that can eventually ...