Content area
There exist two major competing paradigms in computer programming: imperative programming and logic/functional (relational) programming. In this thesis we attempt to formally integrate these approaches. As a consequence of this integration we show that the construction of imperative programs can be first developed and verified in the logic programming paradigm and from this a verifiable imperative program can be derived. We reduce the development of correct imperative programs to developing correct logic programs which are formally associated with the imperative programs. In traditional imperative program verification two distinct notations are used, predicate calculus notation for the program assertions and the imperative program notation itself. An imperative program is verified with respect to some specification written in, in our case, predicate calculus. Our approach to imperative program verification has the advantage of reducing the notations to just that of predicate calculus. We do this by formally associating with an imperative program a logic program in such a way that proving the logic program correct also proves the imperative program correct. In computer terminology, we `inverse compile' an imperative program to a logic program and prove it correct. To formally integrate the imperative and logic programming paradigms we use Dijkstra's notion of weakest precondition which originates in this theory of imperative program verification and development. We formalise this notion of weakest precondition and develop a weakest precondition `calculus' within a set theoretic relational framework and from this develop a theory that enables us to integrate imperative and relational programming. It is through the use of the weakest precondition `calculus' that we are able to associate a relational program with an imperative program. Also we indicate how to use the weakest precondition calculus to formally interpret or symbolically execute imperative programs.