Mechanical Verification of Refactorings

Sultana, Nik, Thompson, Simon (2008) Mechanical Verification of Refactorings. In: Workshop on Partial Evaluation and Program Manipulation. . Assoc of Computing Machinery, NY, USA ISBN 978-1-59593-977-7.


In this paper we describe the formal verification of refactorings for untyped and typed lambda-calculi. This verification is performed in the proof assistant Isabelle/HOL. Refactorings are program transformations applied to improve the design of source code. Well-structured source code is easier and cheaper to maintain, and this motivates the use of refactoring. These transformations have been implemented as programmer tools and, as with other metaprogramming tools, it is desirable that implementations of refactorings are correct. For a refactoring to be correct the refactored program must be identical in behaviour to the original program. Since refactorings are source-to-source transformations, concrete program information matters: for example, names (of variables, procedures, etc) and program layout should also be preserved by refactoring. This is a particular characteristic of refactorings since general program transformations operate over machine representations of programs, rather than readable source code. The paper describes the formalisation adopted, and the alternatives explored. It also reflects on some of the difficulties of performing such formalisations, the interaction between refactoring and phases such as type-checking and parsing, and the generation of correct implementations from mechanised proofs.

Item Type: Conference or workshop item (UNSPECIFIED)
Uncontrolled keywords: Theory, Verification, Refactoring, Isabelle/HOL
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 29 Mar 2010 12:09 UTC
Last Modified: 28 May 2019 15:19 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year