B. Wagle
EJOR
In this paper, we show how refinement calculus provides a basis for translation validation of optimized programs written in high level languages. Towards such a direction, we shall provide a generalized proof rule for establishing refinement of source and target programs for which one need not have to know the underlying program transformations. Our method is supported by a semi-automatic tool that uses a theorem prover for validating the verification conditions. We further show that the translation validation infrastructure provides an effective basis for deriving semantic debuggers and illustrate the development of a simple debugger for optimized programs using this approach using Prolog. A distinct advantage of semantic debugging is that it permits the user to change values at run-time only when the values are consistent with the underlying semantics. © 2005 Elsevier B.V. All rights reserved.
B. Wagle
EJOR
Yvonne Anne Pignolet, Stefan Schmid, et al.
Discrete Mathematics and Theoretical Computer Science
Bowen Zhou, Bing Xiang, et al.
SSST 2008
M.J. Slattery, Joan L. Mitchell
IBM J. Res. Dev