Why Be Formal?

Whereas Parts I and II focused on canonical examples, Part III marches toward complete applications, resplendent with runtime considerations. The current chapter addresses code and compiler correctness. Chapter 11 discusses language interoperability. Chapter 12 addresses scalability and weaves elements of the entire book into a vision for multiphysics framework design.

Formal methods form an important branch of software engineering that has apparently been applied to the design of only a small percentage of scientific simulation programs (Bientinesi and van de Geijn 2005; van Engelen and Cats 1997). Two pillars of formalization are specification and verification – that is, specifying mathematically what a program must do and verifying the correctness of an algorithm with respect to the specification. The numerical aspects of scientific programming are already formal. The mathematical equations one wishes to solve in a given scientific simulation provide a formal specification, whereas a proof of numerical convergence provides a formal verification. Hence, formal methods developers often cite a motivation of seeking correctness standards for non-scientific codes as rigorous as those for scientific codes (Oliveria 1997). This ignores, however, the nonnumerical aspects of scientific programs that could benefit from greater rigor. One such aspect is memory management. The current chapter specifies formal constraints on memory allocations in the Fortran implementation of the Burgers equation solver from Chapter 9.