LM
L. Miljak
Authored
1 records found
The goal of automated refactoring is to reduce maintenance effort. To realize this, programmers need to be able to trust or manually check that refactorings actually preserve behavior. To allow programmers to focus on such checks, automated refactorings should preserve program we
...
Contributed
6 records found
Don’t bind yourself to do notation!
Using Agda to Prove Correctness of Refactorings on Monads
This paper provides a refactoring from do notation to >>= operators and proves that this refactoring maintains observational equivalence. As programs grow ever larger and more complex, there is a growing need to automatically apply refactorings to these programs in a dependable m
...
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 refactorin
...
Maybe a List would be better?
Correct by construction Maybe to List refactorings in a Haskell-like language
This paper concerns itself with correct by construction refactoring of Maybe values to List values in a Haskell-like language (HLL) as a case study on data-oriented refactorings. Our language makes use of intrinsically-typed syntax and de Bruijn indices for variables. Operational
...
Proving correctness of refactoring tuples to records
A correct-by-construction approach on a Haskell-like language
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
...
Formally proving the correctness of the (un)currying refactoring
Using Agda with a simple Haskell-like programming language
When designing critical software, great care must be taken to guarantee its correctness. Refactoring is one of the techniques used to improve code readability, maintainability, and other factors without changing functionality. Thus, to ensure that it is properly applied, automate
...
Refactorings are program transformations that preserve the observable behavior of the program. The refactoring function inlining replaces a function call with the contents of the referenced function definition. To preserve the behavior, properties such as reference relations must
...