When we write programs, we don't always get the code right first time. A function may start off with one purpose that changes to another: the function is now mis-named; we may have chosen a particular way of representing some real-world object as a data structure, but we find that we need to change the representation to make it more general, or adapt to a change in other parts of the organisation. In both cases we need to transform our program, without changing what it already does, even though we change how it does it. This process is called refactoring.
In a program of any size, making the simplest refactoring happen can be complicated. For example, if we rename a commonly used library function this may result in changes in hundreds of files, and making the change can be too costly and error prone to do by hand. For this reason, engineers have built refactoring tools that automate the process of making common refactoring transformations, and these tools can be found for many languages, integrated into programmers' standard workflow (e.g. into the Eclipse IDE for Java). Even so, refactoring tools are used less than might be anticipated: a reason for this is a lack of trust in the tools (see e.g. E Murphy-Hill et al, How We Refactor, and How We Know It, 2012). When we apply a tool, how do we know that it hasn't changed what our program does?
In this project our aim is to make a step change in the way that refactoring tools are built, so that we demonstrably improve the trustworthiness of the way that the tools make the refactorings. For example, in the case of our industrial partners, 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.
How will we achieve this? The UK is a world leader in showing how computers can support logical reasoning, either by answering logic questions automatically (SAT/SMT solvers) or by supporting "by hand" proof (proof assistants such as Isabelle and HOL). In this project we will build on our work in the HOL proof assistant to formally verify a compiler for the CakeML language. This infrastructure will help us to build a refactoring tool for CakeML in which we are able to say, in advance, that a particular refactoring - such as renaming - is guaranteed never to break a program.
While this work advances the state of the art for academic computer science, we also want to support the practising engineer, and so in this project we will work closely with Jane Street Capital, a leading user of the OCaml language, to develop a trustworthy refactoring tool for this industrially-relevant language. This tool 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.
We will ensure the practicality of the tool by working with industrial partners, Jane Street, and embed one of the researchers in industry for part of the project. The refactorings implemented will be chosen to support development not only in our partners, but also in the wider OCaml developer community, and the tool will be freely available under an open source licence, supporting its sustainability beyond the life of the project.
In providing verified refactorings for CakeML we will go beyond the state of the art for program verification, and in the OCaml development, we will set a new benchmark for building refactoring tools for programming languages in general.
|