Skip to main content

Mechanical Verification of Refactorings

Sultana, Nik and Thompson, Simon (2008) Mechanical Verification of Refactorings. In: PEPM '08 Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation. PEPM Partial Evaluation and Program Manipulation . ACM, New York, USA, pp. 51-60. ISBN 978-1-59593-977-7. (doi:10.1145/1328408.1328417) (KAR id:23959)

Language: English
Download (233kB)
[thumbnail of MechThompson.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


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: Book section
DOI/Identification number: 10.1145/1328408.1328417
Uncontrolled keywords: Theory, Verification, Refactoring, Isabelle/HOL
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Funders: Association for Computing Machinery (
Depositing User: Mark Wheadon
Date Deposited: 29 Mar 2010 12:09 UTC
Last Modified: 12 Jul 2022 10:40 UTC
Resource URI: (The current URI for this page, for reference purposes)
Thompson, Simon:
  • Depositors only (login required):


Downloads per month over past year