Semantic refactorings

Refactorings are structured changes to existing software that leave its externally observable behaviour unchanged. The intent is to improve readability, performance or other non-behavioural properties of a program. Agile software engineering processes stress the importance of refactoring to keep program code extensible and maintainable. Despite their apparent benefits, manual refactorings are time-consuming and prone to introducing unintended side effects. Research efforts seek to support and automate refactoring tasks to overcome these limitations. Current research in automatic refactoring, as well as state-of-the-art automated refactoring tools, frequently rely on syntax-driven approaches. They focus on transformations which can be safely performed using only syntactic information about a program or act overly conservative when knowledge about program semantics is required. In this thesis we explore semantics-driven refactoring, which enables much more sophisticated refactoring schemata. Our semantics-driven refactorings rely on formal verification algorithms to reason over a program’s behaviour, and we conjecture they are more precise and can handle more complex code scenarios than syntax-driven ones. For this purpose, we present and implement a program synthesis algorithm based on the CEGIS paradigm and demonstrate that it can be applied to a diverse set of applications. Our synthesiser relies on the bounded model checker CBMC as an oracle and is based on an earlier research prototype called Kalashnikov. We further define our Java Stream Theory (JST) which allows us to reason over a set of interesting semantic refactorings. Both solutions are combined into an automated semantic refactoring decision procedure, reasoning over program behaviours, and searching the space of possible refactorings using program synthesis. We provide experimental evidence to support our conjecture that semanticsdriven refactorings exceed syntax-driven approaches in precision and scope.