Refactoring with confidence

Creating and proving the correctness of a refactoring to add arguments to a function in a functional language

Bachelor thesis (2023)

Authors

K.H. Struik Electrical Engineering, Mathematics and Computer Science

Contributors

J.G.H. Cockx Programming Languages - EEMCS (mentor)
L. Miljak Programming Languages - EEMCS (mentor)
K.G. Langendoen Embedded Systems - EEMCS (graduation committee member)
Faculty
Electrical Engineering, Mathematics and Computer Science, Electrical Engineering, Mathematics and Computer Science
Copyright: © 2023 Kalle Struik
More Info
expand_more

Published Date

30-06-2023

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Faculty

Electrical Engineering, Mathematics and Computer Science

Abstract

Refactoring tools are an important tool for developers, but their reliability can be questionable at times. In this paper, we show that it is feasible to formally verify refactoring tools using computer-aided proofs. To this end, we create a Haskell-like language and a refactoring operation on this language to add an extra function argument to an arbitrary function in the program. And finally, use the Agda proof assistant to construct a proof of the correctness of this refactoring.

Files

Refactoring_with_confidence_kh... (pdf)
(pdf | 0.173 Mb)
Unknown license