A comparative study of pre/post condition and relational approaches to program development

With so many software-related failures happening these days, there is an increasing demand for software quality. Rigorous development approaches, which apply mathematical techniques to the design and implementation, should be getting more consideration as one of the solutions to software reliability. Pre/postcondition approaches and relational approaches are two groups of influential rigorous techniques. Both of them use classical mathematical concepts to describe and simplify programming objects. To further propel the application of these approaches, their relative strengths and limitations in terms of practicability and accessibility need to be identified and elaborated. In this thesis, we conduct a comparative study between the pre/postcondition approaches, proposed by Floyd, Hoare, Dijkstra and Baber, and the relational approaches, proposed by Mills and Parnas. We investigate aspects related to their mathematical models. Their abilities of specifying different termination behaviours, dealing with non-determinism, distinguishing between specifications and descriptions, etc. are discussed. Some practical issues, such as considerations on common programming constructs, side effects, verification procedures, etc. are reviewed. The comparison criteria are grouped into two categories – theory and practice. Under each criterion, we illustrate and evaluate the strength or weakness of each approach. Suggestions regarding the applications of these approaches are also presented.