Current tools for pattern matching computer programs often operate on abstract syntax trees or other static representations of programs. These approaches, though efficient, are fundamentally limited when it comes to capturing the dynamic behavior of programs. For example, it is not always possible to express (concise) syntactic patterns that capture programs which are semantically equivalent but differ in their syntactic representation. A tool that takes into account the behavior (or dynamic semantics) of programs would be able to capture programs that are semantically equivalent in a more concise manner with a single pattern. Additionally, taking into account program behavior leads to more precise pattern matching, by excluding unreachable paths of computation. In this thesis, we explore a novel method, based on behavioral models of programs, that allows patterns to take into account the dynamic semantics of a program. We propose the Dyno pattern language, in which concrete object language syntax can be used to express intuitive semantic patterns of programs. Pattern matching is performed by translating Dyno patterns to μ-calculus formulas and model checking these formulas against models extracted from object programs. Because our method is based on dynamic models of programs, we are fundamentally limited by the halting problem. In favor of precision, our method compromises on efficiency and termination guarantees. In particular, termination is not guaranteed when the extracted model of a program has infinitely many states. To recover termination in some cases, we provide the facility to express bounds on input parameters, limiting the search space while compromising on soundness. We recognize some limitations in our work, including a lack of match evidence (e.g. the location of a match in the object program’s syntax tree), as well as holes in Dyno’s expressiveness. To address the latter issue, we suggest operators that could be added to Dyno in the future.

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.

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.

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 semantics are defined using big step semantics. We define a refactoring function which intrinsically verifies its well-typedness due to our intrinsically-typed syntax. The semantic validity of this refactoring is given by a separate proof. We use Agda, a functional language and theorem prover, to define and prove these properties. Techniques and concepts used in our refactoring and proof generalize well to other data-oriented refactorings.

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, automated tools are used to perform refactoring. To ensure that the code remained correct, we verified the correctness of the tool actions using formal proof. This is assisted by a dependently typed language Agda, which, when used as a proof assistant, can directly support us by ensuring the soundness of the steps taken. We consider the refactoring of currying and its counterpart, uncurrying, using a small proof-of-concept functional programming language with intrinsically typed terms and de Bruijn indices. Furthermore, we proved the retained properties of well-typedness, termination, and value relation of the input program. Finally, we argue that this research could be extended to the full implementation of Haskell, as well as applied to other languages and similar refactorings.

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 manner. Current refactoring engines often contain errors, even if they are widely used and thoroughly tested. The methods used in the proof of contextual equivalence are described in this paper, with the goal of supporting future research into correct-by-construction refactorings.

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 be retained and language constructs like 'return' statements must be replaced. Implementing a behavior preserving refactoring is a time-consuming and error-prone task. In the past, such refactorings have only been implemented for one language at a time, thus they cannot be reused in other languages.

This thesis presents a language parametric function inlining algorithm that can be applied to any language. The algorithm performs function inlining and checks the transformed program for static semantics errors and changes to reference relations that would cause a change to the behavior of the program, fixing them where possible. The required language parameters are an AST parser, a static semantics analyzer that can derive reference relations, and a set of language-specific functions that can perform language-specific tasks, for example identifying return statements.
An implementation of the algorithm is provided in the language workbench Spoofax using the transformation language Stratego. It can be applied to all languages with an SDF3 defined grammar and a Statix semantics analyzer. The implementation is tested on C++, WebDSL and Tiger using unit tests.