###
A Comparative Study of Pre/postcondition and Relational Approaches to Program Development

####
Hong Duan

Abstract

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.