Donald Bren School of Information and Computer Sciences

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.