Web APIs are being used for increasingly larger and complex use cases. Right now it can be hard to make sure that what is documented about an API is correct everywhere and to know if a change will have impact on the users of a web API. When details are missing in an API specification users of that API need to make assumptions about how the API works. The creators of the web API also wants to know what users expect from the API. There are two sides to this problem, enforcing that the implementation is actually the same as what is specified, and making it possible to define API specifications as precise as possible. The type system of a programming language is a useful tool for enforcing the struc- ture of an implementation. In this thesis we use a dependent type system to enforce an API specification in the implementation. By using the dependent type system we can de- fine additional, more specific, constraints on the API. These constraints are more specific than constraints expressible in possible research. With this approach we can be sure that the specification and implementation are actually describing the same API. And with the added flexibility we can create a more complete description of web APIs.

Pattern matching is the act of checking if a value is in the set of values described by a pattern. Many programming languages provide constructs to pattern match on program values. Pattern matching constructs appear in different variants. Stratego, a term rewriting language, features first-class pattern matching, which attempts to match a pattern with a value. If the match is successful, variables in the pattern are bound. If the pattern does not match, the matching expression fails. Using choice and sequence operators, one can build expressions that attempt to match multiple patterns until a match succeeds, evaluating the expression that corresponds to that pattern. This is a common way of branching in Stratego programs. The Stratego compiler handles each match attempt independently, disregarding the context.

In this thesis, we research context-aware compilation of first-class matches, aiming to speed up pattern matching operations without requiring changes to programs. We research the resemblance of Stratego pattern matching with match cases, a pattern matching construct that is ubiquitous in functional-style languages. Previous research shows that match cases can be compiled efficiently by considering all cases together, instead of a single alternative at the time, during compilation. We develop behaviour-preserving translations from first-class matches to match cases and from match cases to decision tree automata. We efficiently represent these automata in Java, the target language of the Stratego compiler. All these changes integrate in the latest upstream version of the Stratego compiler.

We evaluate the performance of our altered compiler and observe an average speed-up of 4x on programs that rely heavily on pattern matching, at the cost of a 20% increase in compilation time and space.

JSGLR2 is a modular Java implementation of the SGLR parsing algorithm that supports systematic benchmarking and improvement of its several parsing variants. By splitting the code into several components, they can be tested in isolation and thus optimized more effortlessly. The modular architecture, although beneficial for efficiently identifying and implementing optimizations, negatively impacts the performance of the parsing algorithm. This paper aims to measure the overhead introduced by the code architecture for one of the variants, more specifically the incremental variant, which combines incremental parsing with SGLR parsing. It does so by comparing the original implementation with a version with the modularity removed. The evaluation is done on programming languages used in practice: Java, WebDSL and SDF3. The results show that the inlined parser outperforms the previous one, achieving speedups of up to 16% in batch parsing and up to 10% in incremental parsing.

Due to the increase in student numbers, the amount of time teachers have for each individual decreases. To keep the quality of the program the same, learning analytics can be utilized to assist teachers to give a better overview of problems which the students are struggling the most with. This work makes use of WebLab data of the Introduction to Python course. To provide more useful information for teachers in introductory programming assignments, this work applies learning analytics to revision history of the student submissions of this course. The revision history provides more insight into the progression of the students throughout the assignment compared to only the final solutions. With these data, this work clusters and analyzes student submissions to provide instructors with information about the types of submitted solutions, students who struggled with the assignment, and the biggest hurdles for the students. Results show that the clustering of student submissions is 90\% accurate in comparison to manually clustered solutions, however the identification of students who struggled with the assignment should take student behaviour more into account. Because, student behaviour has been discussed in the focus group as being a major factor in whether data can indicate whether a student is struggling or not. Further research should be directed into expanding the proposed algorithms to more complex programming assignments and improving the way the data is visualized to the teachers.

JSGLR2 is a java implementation of the Scannerless Generalized LR-parsing (SGLR) algorithm. It employs a modular architecture. This architecture comes with a performance overhead for letting multiple components interact with each other. This paper looks into the size of the performance overhead penalty for the recovery parser variant. It does so by creating an 'inlined' version of the recovery parser variant. The inlined recovery variant is a JSGLR2 implementation that ignores the modular architecture, and hard-codes the components. The performance of the inlined variant is measured with a pre-existing evaluation suite. The results show that there is a performance increase between the original, and the inlined variant.

Refactoring is the process of improving the structure of code without changing its functionality. The process is beneficial for software quality but challenges remain for identifying refactoring opportunities. This work employs machine learning to predict the application of the refactoring type Extract Method in an industry setting with the use of code quality metrics. We detect 919 examples in industry code of Extract Method and 986 examples where Extract Method was not applied and compare this to open-source code. We find that feature distributions between industry and open-source code differ, especially in class-level metrics. We train models to predict Extract Method in industry code and find that Random Forests perform best. We find that class-level metrics are most important for the performance of these models. We then investigate whether models trained on an open-source set generalize to an industry setting. We find that, although less performant than a custom fit model, a Logistic Regression type model performs admirably. Afterward, we examine whether these models perform on unseen industry projects by validating on projects excluded from the training set. We find that average performance is decent but lower than when using the whole industry dataset or an open-source dataset for training. Lastly, we conduct a blind user study in which we ask experts to judge predictions made by our best model. We find that experts generally agree with the model's predictions. In the case that experts agree with the model's prediction to apply Extract Method, they do so because of high code complexity. When they agree with the model's prediction not to refactor they most frequently give the reason that the respective methods are already sufficiently understandable.

The cloud is widely adopted as a flexible and on-demand computing infrastructure. In recent years, a new and promising cloud paradigm emerged: serverless computing. Serverless computing promises a pay-as-you-go model and offers features such as autoscaling and high availability. Nevertheless, developing scalable cloud applications remains a painstaking task. Currently, programming models for the cloud mix operational code and business logic causing developers to spend a significant amount of time on other tasks rather than implementing the intended functionality. Moreover, the developer must consider distributed systems concerns such as consistency, communication, and persistence. Modern dataflow systems, such as Apache Flink and Google Dataflow, address these concerns but suffer from the same problem: they lack an intuitive programming interface for general-purpose applications. It remains an open problem to design a developer-friendly programming interface for implementing scalable cloud applications with strong guarantees.

In this thesis, we solve this problem by presenting an intuitive programming interface for scalable cloud applications in which developers primarily focus on business logic. Given a set of easy-to-follow code conventions, programmers author stateful entities a programming abstraction embedded in Python. We present a compiler pipeline named StateFlow, to analyze the abstract syntax tree of a Python application and rewrite it into an intermediate representation based on stateful dataflow graphs. In addition, we present a set of building blocks that allow the execution of this intermediate representation on a target runtime system or cloud provider without a tight integration. Supported runtime systems include Apache Flink and Beam, AWS Lambda, Flink's Statefun, and Cloudburst, each providing a different set of guarantees. Finally, we introduce a client-side programming interface and HTTP server integration to interact with the deployed application.

We demonstrate that the execution with StateFlow typically incurs less than 1\% overhead. Furthermore, we identify limitations of current dataflow systems in executing cloud applications at scale in a performance benchmark. Finally, we compare the expressiveness of StateFlow's programming abstraction to native runtime implementations. We show that StateFlow lets a developer write universal code that does not mix business with operational logic or the runtime's API and prevents vendor lock-in by allowing them to switch between runtimes in less than ten lines of code.

Procedural content generation (PCG) for architecture is widely used in a variety of digital media, most notably in games. However, such methods are often limited in their expressive range, and require considerable technical knowledge to create non-trivial architectural structures. We present a novel tile-based PCG approach for generating architecture, that proposes the use of architectural profiles, a declarative characterization of architectural typology, within a generic tile solving framework. An architectural profile consists of a set of tiles, representing atomic architectural building blocks, and a set of declarative constraints and rules, specifying which conditions a tile configuration has to satisfy to be valid. These conditions are translated into logic constraints, and used by a tile solver to control tile placement in a bottom-up manner. Eventually, each valid model output by the solver is a representative instance of its architectural profile. We describe an implementation of this approach with Answer Set Programming, using an off-the-shelf constraint solver for model generation. We performed an expressive range analysis, and concluded that our declarative method is quite controllable and can be steered over a broad range of architectural structures, regarding density and repetitiveness. Due to this expressive range and control, our tile-based method is very suitable for the customized development of urban environments for games. We also explore the adaptability of architectural profiles by application on pre-existing terrains.

Context:
Updating an old result by selective re-execution of the inconsistent
parts of some computation is usually faster than recomputing everything.
Incremental build systems and interactive development pipelines
use this technique to speed up feedback.
They consist of different tasks.
These tasks form a graph by depending on the environment and the result of other tasks.
To re-execute a build requires an incremental build algorithm to find and re-execute inconsistent tasks.
This can be done by traversing the dependency graph top down.
When the mutations to the input environment are known in advance a
build algorithm can avoid graph traversal. Thereby scaling with the size of a change instead of the size of the graph.
Another important distinction between incremental build systems is their ability to handle dynamic dependencies.
That is, dependencies that are discovered during a build.
PIE is a bottom-up build algorithm that supports dynamic task dependencies.
It schedules and executes inconsistent tasks without traversing the entire dependency graph.
The current PIE algorithm is capable of adding dynamic task dependencies.
However, it does not process removing dynamic task dependencies.
This preserves consistency, but limits scalability over time.
Each detached task is still scheduled and executed by the bottom up algorithm.

Inquiry:
PIE is inefficient when it executes tasks that are no longer a transitive dependency.
In this paper we introduce task observability to solve this.
This problem is unique to bottom up scheduling build systems.
However, we are able to re-use techniques from incremental build systems and garbage collections to implement our solution.

Approach:
We split the problem into three parts, determining task observability, scheduling, and re-observing.

Knowledge
With the new algorithm we are able to improve the efficiency of PIE and its scalability over time.

Grounding:
We verify and benchmark our changes with two artificial and one real world use case in the Spoofax Workbench.

Importance:
The PIE runtime is able to continue operating efficiently even when tasks are detached.
In some situations the Spoofax PIE pipeline reduces the feedback time with 1800 ms when results are not observed by the user.
Additionally, new design patterns are made possible.
For Spoofax, toggling observability creates the opportunity to implement various quality of life features such as file and project renaming.

As a secondary contribution we implement a garbage collector for detached tasks and create a visualization tool for displaying the dependency graphs stored in PIE.

Large companies suffer from the increasing complexity that exist in their software systems. Evolving their software becomes even harder if we consider that a change in one system can affect several other parts of their software architecture. Especially banks that need to be always complied with regulations, have to constantly make changes in their software to reflect these changes. ING is a primary example that currently tries to find a solution to these problems through the use of model driven development and more specifically code generation. In particular, they have created a Domain Specific Language called Maverick to specify the requirements/business logic and through the usage of code generators to automatically generate their entire codebase from these Maverick specifications. Code generators as any other software artifact is not bug free, meaning that testing code generators is of paramount importance. However, testing code generators is not straightforward as their output is another program that besides syntactic structure also has behavior. Many formal approaches have been developed that try to formally prove the correctness of code generators. Nevertheless, the complexity and scalability issues that these approaches face make them infeasible in practice. This thesis presents a testing approach that leverages a definitional interpreter to test code generators. We evaluate and show the practicability of our approach using Maverick specifications developed by ING and we conclude that our proposed method can address many of the issues that formal approaches face.

Session types are a formal method to describe communication protocols between two or more actors. Protocols that type check are guaranteed to respect communication safety, linearity, progress, and session fidelity. Basic session types, however, do not in general guarantee anything about the contents of messages, while real-life applications of structured communication, such as money transfers at the ING bank, could benefit greatly from content safety. In this work, we show how to state, verify, and run session-typed protocols with dependent variables in Idris, using Idris’ ST library.
We also present an extension to the protocol description language Scribble. Scribble is a language for defining high-level global protocols between multiple actors and comes with a tool that automatically generates type signatures of local protocols for each actor in Java, in a way that these type signatures ensure that local actors follow the global protocol specification. We describe a new variant of the Scribble language which adds support for dependent variables, and a new tool for automatically generating Idris type signatures of local protocols for actors in a way that enforces dependent invariants.

When using an integrated development environment, it is desirable to get real-time feedback on the correctness of the program. That is, we want to see the results of the type checker in real-time. However, type checking can take a long time, especially when the subject program is large. To be able to provide real-time results, we need to incrementalize the type checker. This way, when a program changes, we only need to recalculate results for the changed portion of the program, and everything that depends on it. In this thesis, we discuss how we used IncA to implement a type checker for Rust. IncA is a domain specific language for the definition of incremental program analyses: analyses written in IncA are automatically incrementalized. We show in our evaluation that our type checker updates results significantly faster than its non-incremental counterpart. While we were able to successfully implement many of Rust's features, there are some parts we were unable to implement, and we show why that is the case.

Many program transformation languages simplify the implementation of program transformations. However, they give only weak static guarantees about the generated code such as well-sortedness. Well-sortedness guarantees that a program transformation does not generate syntactically ill-formed code, but it is too imprecise for many other scenarios. In this paper, we present a static analysis that allows developers of program transformations to reason about their transformations on a more fine-grained level, namely that of syntactic shape. Specifically, we present an abstract interpreter for the Stratego program transformation language that approximates the syntactic shape of transformed code using regular tree grammars. As a baseline, we also present an abstract interpreter that guarantees well-sortedness. We prove parts of both abstract interpreters sound.

For programs controlling industrial processes, it is of vital importance that they produce results conform their functional specification. Furthermore, it is important that their running times are bounded, and that we can predict corresponding worst-case scenarios. Programs written in general purpose programming languages can crash or produce erroneous output. Data modeling and query languages are typically more restrictive. However, they either do not guarantee soundness (where values are of a predefined indivisible type) or functional correctness (including deterministic output). Alternatively, they have unbounded or unpredictable worst-case running times, or have limited expressiveness.

We present AlanLight, a data modeling language for expressing complex recursive calculations, while guaranteeing soundness, functional correctness, and polynomial time complexity in the size of user data. To achieve this, we use complex referential integrity constraints and an elegant, formally defined analysis over constraint and calculation definitions in AlanLight programs. Furthermore, we give a formal specification of the dynamic semantics of AlanLight, implying its guarantees, and demonstrating support for on-demand minimal effort calculation.

WebLab is a system where students can write and test code using an online interface. Course coordinators can create assignments and exams, where they can define automated tests to verify that the student code meets requirements. As WebLab only offered support for programming languages which run on the Java Virtual Machine, it was limited to a specific set of languages. In this project, we have designed a system which enables WebLab to support arbitrary languages, while still being able to guarantee scalability, security and reliability. To limit the scope of this project, the focus was laid on the programming language Python. The designed system uses Docker containers to execute arbitrary code in a safe and isolated way. A test fuzzing system with tamper detection is used to achieve reliable test results. The system is flexible as support for new programming languages can be added with relatively little effort. This report describes the design of the system, the research that was done and the process used. The report concludes with recommendations for future work on this project.