The process of using formal verification, in order to ensure that a piece of software meets it functional requirements consists of three main steps: designing a model of the given piece of software, translating the functional requirements, which the piece of software must satisfy, into properties of said model and verifying that the model satisfies those properties. Traditionally, regardless of whether the piece of software is developed based on a predesigned model or the piece of software is developed first and its model is designed after that, the piece of software and its model are two separate entities. Therefore, aside from checking that the model satisfies its properties, it must also be verified that the model accurately represents the given piece of software. While this task may initially seem simple, it gets progressively more difficult, as the piece of software becomes more complex. And, if it turns out that the model is not accurate, then the entire formal verification process is invalid, since it does not provide any guarantees about the actual piece of software. In this thesis we present a solution to this problem: a way of modelling sequential effectful programs, such that the resulting models can be directly translated into runnable programs, thereby guaranteeing the models' accuracy. We achieve this by using algebraic effects, in order to model sequential effectful programs as instances of the coinductive free monad, that could then be translated into runnable pieces of software by applying the necessary effect handlers. Furthermore, we demonstrate that it is possible to express functional requirements as properties of such models using the first-order modal μ-calculus, a fixed-point dynamic logic which has previously been used to reason about labelled transition systems (e.g. in mCRL2).

Effect handler oriented programming (EHOP) is a recently proposed programming paradigm, which aims to provide a separation of concerns by isolating the handling of side-effects from the main application logic. Nowadays, as the core concepts behind EHOP are being added to more and more programming languages, it is evident that EHOP is slowly but steadily growing in popularity. Therefore, it is important to explore the applicability of EHOP for different areas of software development. However, so far, very little research has been conducted on this topic and, thus, barely any possible application domains of EHOP have been investigated. This study focuses on a potential field of application of EHOP, which has not been covered by previous research, namely - text-based game development, and aims to determine the extent to which the usage of EHOP for text-based game development affects the modularity, readability and maintainability of the source code. This goal will be achieved by performing both a qualitative as well as a quantitative analysis of the source code of a text-based game, written in Koka - a state-of-the-art programming language, which supports EHOP. The results show that there are substantial benefits to using EHOP for text-based game development. It significantly improves the modularity, readability and maintainability of the source code at the cost of very little to no performance.