Donald Bren School of Information and Computer Sciences
Correctness of program transformations via the weakest pre-condition formalism of Dijkstra
- Author(s): Kibler, Dennis
- et al.
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.