Program Optimization Using Invariants

Optimizing a computer program is defined as improving the execution time without disturbing the correctness. We show how to use invariants from a proof of correctness in order to change the statement in and around the program´s loops. This approach is shown to systematize existing optimization methods, and to sometimes allow stronger optimizations than are possible under the standard transformation approach.