Specification, implementation and verification of refactorings
2010
Refactoring is the process of reorganising or restructuring code by
means of behaviour-preserving program transformations, themselves
called refactorings. Most modern development environments come with
built-in support for refactoring in the form of automated refactorings
that the user can perform at the push of a button. Implementing
refactorings is notoriously complex, however, and even
state-of-the-art implementations have very low standards of
correctness and can introduce subtle changes of behaviour into
refactored programs.
In this thesis, we develop concepts and techniques that make it
possible to give concise, modular specifications of
refactorings. These specifications are precise enough to cover all
details of the object language, and thus give rise to full featured,
high-quality refactoring implementations. Their modularity, on the
other hand, makes them amenable to formal proof, and hence opens the
door to the rigorous verification of refactorings.
We discuss a disciplined approach to maintaining name bindings and
avoiding name capture by treating the binding from a name to the
declaration it refers to as a dependency that the refactoring has to
preserve. This approach readily generalises to other types of
dependencies for capturing control flow, data flow and synchronisation
behaviour.
To implement complex refactorings, it is often helpful for the
refactoring to internally work on a richer language with language
extensions that make the transformation easier to express. We show how
this allows the decomposition of refactorings into small
microrefactorings that can be specified, implemented and verified in
isolation.
We evaluate our approach by giving specifications and implementations
of many commonly used refactorings that are concise, yet match the
implementations in the popular Java development environment Eclipse in
terms of features, and outperform them in terms of correctness.
We give detailed informal correctness proofs for some of our
specifications, which are greatly aided by their modular
structure. Finally, we discuss a rigorous formalisation of the central
name binding framework used by most of our specifications in
the theorem prover Coq, and show how its correctness can be
established mechanically.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
0
References
0
Citations
NaN
KQI