Mechanical Verification of Refactorings

Sultana, Nik and Thompson, Simon (2008) Mechanical Verification of Refactorings. In: Workshop on Partial Evaluation and Program Manipulation, Jan 07-08, 2008, San Francisco, CA,. (Full text available)

PDF
Download (233kB)
[img]
Preview

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.

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 > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 29 Mar 2010 12:09
Last Modified: 06 Sep 2011 04:50
Resource URI: http://kar.kent.ac.uk/id/eprint/23959 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year