Correctness of program transformations via the weakest pre-condition formalism of Dijkstra
Dennis F. Kibler · eScholarship (California Digital Library) · 1976
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.