Proving correctness of refactoring tuples to records
A correct-by-construction approach on a Haskell-like language
J. Bastenhof (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Jesper Cockx – Mentor (TU Delft - Programming Languages)
L. Miljak – Mentor (TU Delft - Programming Languages)
Koen Langendoen – Graduation committee member (TU Delft - Embedded Systems)
More Info
expand_more
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.
Abstract
Refactoring is a useful tool for increasing the overall quality of software without making changes to how it interacts with the environment. To verify that a refactoring operation correctly transforms an expression, one can provide a formal proof. Using Agda, a dependently-typed language, as a proof assistant, we investigate the feasibility of proving the correctness of refactoring tuples to records for a small-scale language that shares similarities with Haskell. We construct this language in Agda using intrinsically-typed terms and define an accompanying refactoring function for refactoring tuples to records. We prove that the refactoring is well-typed and that it replaces all tuple occurrences. Big-step semantics are used to show the relation between the intrinsically-typed language and its resulting output value. Additionally, we show that we can construct a relation between the values of an expression before and after refactoring. By presenting these proofs we gain more insights into the feasibility of proving the correctness of tuple to record refactoring. Furthermore, we argue that the proofs given for this small-scale language can serve as inspiration for proving comparable properties of the refactoring in the context of Haskell and beyond.