Refinement calculus: A basis for translation validation, debugging and certification

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.