Trustworthy Refactoring

 
 

This is the home page for the Trustworthy Refactoring project in the School of Computing at the University of Kent. The work builds on our experience of designing and building refactoring tools (HaRe and Wrangler) as well as the verified programming language infrastructure in the CakeML project. The project is supported by EPSRC, grant EP/N028759/1.


The project team consists of investigators Scott Owens and Simon Thompson, and research associates Hugo Férée and Reuben Rowe.

 

Refactorings are program transformations that are meant to improve how a program works without changing what it does. Refactorings are not simply search/modify edits. Their successful implementation relies on a knowledge of the meaning of the language; this includes its type system and its module and binding structure as well as its control and data flow. Because refactoring tools transform the code base itself, there is concern about whether they can be trusted, and that concern is well-founded: a study comparing the Java refactoring tools in Eclipse and NetBeans found more than 20 errors in the implementation of common refactorings in each tool.


The overall goal of this project is to investigate the design and construction of trustworthy refactoring tools. When refactorings are performed, the tools will provide strong evidence that the refactoring has not changed the behaviour of the code, built on a solid theoretical understanding of the semantics of the language. This will establish a step change in the practice of refactoring.  For example, in the case of our industrial partners Jane Street, who are among the heaviest users of functional programming worldwide, code changes need to be reviewed by up to three reviewers, and even a straightforward refactoring can give a substantial review overhead. This project will allow reviewers to assure themselves of the safety of changes with substantially less effort.


Our approach will provide different levels of assurance from the (strongest) case of a fully formal proof that a refactoring can be trusted to work on all programs, given some pre-conditions, to other, more generally applicable guarantees, that a refactoring applied to a particular program does not change the behaviour of that program.


The project will make both theoretical and practical advances. At one extreme, we will build a fully-verified refactoring tool for CakeML – a relatively simple, but full featured programming language – and at the other we will build an industrial-strength refactoring tool for OCaml – a related industrially-relevant language. The OCaml tool will allow us to explore a range of verification techniques, both fully and partially automated, and aims to set a new benchmark for building refactoring tools for programming languages in general.


The proposal is timely in bringing together current research in verification – namely the CakeML language and its verified infrastructure – with developments in software tool building. Refactoring tools are becoming more complex, but an inhibitor to their take-up in practice is a perceived lack of trustworthiness: “several developers mentioned that they would avoid using a refactoring tool because of worries about introducing errors or unintended side-effects”.


The CakeML infrastructure is now at a stage where it can be used, rather than further developed, to underpin building refactoring tools with extended assurance built in. This application not only provides better tools to the software engineer, but also allows the CakeML initiative to be evaluated in a project that goes beyond proof of concept to validate the CakeML approach and system.

Project overview