Correctness of program transformations via the weakest pre-condition formalism of Dijkstra

Dijkstra's weakest pre-condition formalism for proving correctness of programs is modified and extended to show the validity of several source-to-source transformations. Examples of the method developed include transformations involving goto elimination, loop fusion and splitting, distribution over conditionals, commutativity of statements, and removal of the empty statement