KS
K.H. Struik
info
Please Note
<p>This page displays the records of the person named above and is not linked to a unique person identifier. This record may need to be merged to a profile.</p>
1 records found
1
Refactoring with confidence
Creating and proving the correctness of a refactoring to add arguments to a function in a functional language
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.
...
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.