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

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

  • Author(s): Kibler, Dennis
  • et al.
Abstract

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
Current View