Verification of Optimizing Algorithms Based on Naive Denotational Semantics

摘要

All too often the run-time behavior of optimized code is inconsistent with the pre-optimization behavior. The paper presents a framework in which optimizing algorithms for imperative programs can be proved to be correct. The correctness proofs are based on specifications which follow the lines of naive denotational semantics. (Copyright (c) GMD 1991.)