Context handling in the Refinement Calculus framework
Linas Laibinis, Joakim Wright von · 1997
We describe two approaches for context handling in the Refinement Calculus framework. They show how information relevant for total correctness can be transported from one place of a program to another and then used for refinement of program components. Both approaches have been formalised in the HOL theorem proving system and integrated into a tool for transformational reasoning about programs. TUCS Research Group Programming Methodology Research Group 1 Introduction The Refinement Calculus [2, 3] is a calculus for development of programs using the stepwise refinement paradigm. In the Refinement Calculus, specifications are refined into programs through a sequence of transformations (refinements). Each such refinement provably preserves all total correctness properties of the initial specification. Programs can be very large and complex. Therefore, it is usually very difficult to prove refinement of the whole program directly. Instead, one can refine a program by focusing on some sm...