Verification of Refactorings in Isabelle/HOL

Sultana, Nik (2008) Verification of Refactorings in Isabelle/HOL. Other masters thesis, Computing Laboratory, University of Kent. (Full text available)

Download (960kB) Preview


Refactorings are source-to-source behaviour-preserving program transformations that are used for improving program structure. Programmers refactor code to adapt it when new functionality is added or when the code is being repaired -- refactoring serves to keep the code ``clean'' and more maintainable. Refactoring can also be used as an exploratory technique for understanding source code. The process of refactoring has been automated through the implementation of tools; these tools assist programmers by handling the consistent application of behaviour-preserving changes to the code. It is desirable that the implementations of refactorings are correct: bugs might otherwise be introduced in refactored programs. The correctness, i.e. behaviour-preservation, of refactoring is traditionally probed by testing the refactored program and not the refactoring implementation directly. Recently, automated testing techniques have been used to test implementations of refactorings directly, but the coverage of testing is partial at best. The verification of refactorings is more challenging but determines whether a refactoring is behaviour-preserving for all possible programs. We study the verification of refactorings using the proof assistant Isabelle/HOL for untyped and typed lambda-calculi. Some of the issues encountered during verification are technical rather than purely theoretical: they relate to the embedding of the programming language in the proof environment. The reasons for our choice of techniques are discussed. We also discuss other practical considerations such as the readability of mechanised refactorings, and the avoidance of computationally expensive refactorings.

Item Type: Thesis (Other masters)
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: 06 Sep 2011 04:51 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year