School of Computing

Mechanical Verification of Refactorings

Nik Sultana and Simon Thompson

In Workshop on Partial Evaluation and Program Manipulation, pages 182-196. ACM SIGPLAN, January 2008.

Abstract

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.

Download publication 213 kbytes

Bibtex Record

@inproceedings{2635,
author = {Nik Sultana and Simon Thompson},
title = {{M}echanical {V}erification of {R}efactorings},
month = {January},
year = {2008},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2008/2635},
    publication_type = {inproceedings},
    submission_id = {24359_1196361019},
    booktitle = {Workshop on Partial Evaluation and Program Manipulation},
    organization = {ACM SIGPLAN},
    refereed = {yes},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014