Skip to main content
Open Access Publications from the University of California

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.

Main Content
For improved accessibility of PDF content, download the file to your device.
Current View